other simplifications.

diff --git a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
index 9751143068b5790e894772c2264c2d5c688d5702..7a68a5bd8530f1dbfd8929df7038b89fd4e20779 100644 (file)
--- a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
+++ b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
@@ -102,8 +102,7 @@ apply (le_times_to_le c (a/c) a)
 [ assumption
 | rewrite > (sym_times c (a/c)).
   rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?)
-  [ rewrite < (sym_times a c).
-    apply (O_lt_const_to_le_times_const).
+  [ apply (le_times_n c a ?).   
     assumption
   | assumption
   | assumption
@@ -152,18 +151,6 @@ cut(O \lt c)
 ]
 qed.
 
-(*
-theorem div_times_to_eqSO: \forall a,d:nat.
-O \lt d \to a*d = d \to a = (S O).
-intros.
-apply (inj_times_r1 d)
-[ assumption
-| rewrite > sym_times.
-  rewrite < (times_n_SO d).
-  assumption
-]
-qed.*)
-
 
 theorem div_mod_minus:
 \forall a,b:nat. O \lt b \to
@@ -175,22 +162,6 @@ rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
 ]
 qed.
 
-(*
-theorem sum_div_eq_div: \forall a,b,c:nat.
-O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
-intros.
-elim H2.
-rewrite > H3.
-rewrite > (sym_times c n2).
-rewrite > (div_plus_times c n2 b)
-[ rewrite > (div_times_ltO n2 c)
-  [ reflexivity
-  | assumption
-  ]
-| assumption
-]
-qed.
-*)
 
 (* A corollary to the division theorem (between natural numbers).
  *

diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma
index b4612034197796218a6068ddce844938f709656e..5ce43d4ac0c968e8006ffb2c5685864fca904321 100644 (file)
--- 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))