X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftotient1.ma;h=5ce43d4ac0c968e8006ffb2c5685864fca904321;hb=c187392ea5521aa5daf86be2ed947016493fed79;hp=b4612034197796218a6068ddce844938f709656e;hpb=e65e31bab82994cf8400bb4c294cf7d16fa2c83c;p=helm.git

diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma
index b46120341..5ce43d4ac 100644
--- a/helm/software/matita/library/nat/totient1.ma
+++ b/helm/software/matita/library/nat/totient1.ma
@@ -362,17 +362,11 @@ cut (O \lt n)
     ]
   | assumption
   ]
-| apply (nat_case1 n)
-  [ intros.
-    rewrite > H7 in H6.
-    rewrite > sym_times in H6.
-    simplify in H6.
-    rewrite > H6 in H.
-    apply False_ind.
-    change in H with ((S O) \le O).
-    apply (not_le_Sn_O O H)
-  | intros.
-    apply (lt_O_S m)
+| apply (divides_to_lt_O n c)
+  [ assumption
+  | apply (witness n c b).
+    rewrite > sym_times.
+    assumption
   ]
 ]
 qed.
@@ -573,7 +567,7 @@ apply (trans_eq ? ?
               | apply (sum_divisor_totient1_aux2);
                 assumption
               ]
-            | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).    
+            | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)).
               apply (andb_true_true 
               (eqb (gcd (i\mod n) (i/n)) (S O))
               (leb (S (i\mod n)) (i/n))