X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ftotient.ma;h=a86986a81f743efd78b0dd004e38653c0788d601;hb=01b688447c18c1992b0c19ac5583ca9fee692514;hp=730ec8b56cfc05bad765600ccad3418e5d71dbac;hpb=6c8f66d57aa3da3b91ff6c76442424dfe2eeceaf;p=helm.git

diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index 730ec8b56..a86986a81 100644
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -24,7 +24,7 @@ include "nat/iteration2.ma".
     phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
    (so this definition considers the values i=1,2,...,n)
   
-  sigma_p doesn't work ok the value n (but the first value it works on is (pred n))
+  sigma_p doesn't work on the value n (but the first value it works on is (pred n))
   but works also on 0. That's not a problem, in fact
    - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. 
    - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. 
@@ -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]
@@ -133,4 +134,4 @@ apply (nat_case1 n)
        ]
      ]
    ]
-qed.
\ No newline at end of file
+qed.