Prototype of min_aux changed.

[helm.git] / matita / library / nat / totient.ma

diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index 730ec8b56cfc05bad765600ccad3418e5d71dbac..03e2587a8f02b1bc17eb3f3e8d0a8f932ad5417c 100644 (file)
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -63,7 +63,8 @@ apply (nat_case1 n)
    [intros.unfold cr_pair.
         apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
           [unfold min.
-           apply le_min_aux_r
+           apply transitive_le;
+            [2: apply le_min_aux_r | skip | apply le_n]
           |unfold lt.
            apply (nat_case ((S m2)*(S m1)))
             [apply le_n|intro.apply le_n]