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

diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma
index feaf1314b..5ce43d4ac 100644
--- a/helm/software/matita/library/nat/totient1.ma
+++ b/helm/software/matita/library/nat/totient1.ma
@@ -96,7 +96,6 @@ cut (O \lt (pred n))
 ]
 qed.
 
-
 (*3rd*)
 theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat.
 i < n*n \to (divides_b (i/n) (pred n) \land
@@ -137,7 +136,7 @@ apply divides_SO_n.
 qed.
 
 theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
-i < n*n \to 
+(S O) \lt n  \to i < n*n \to 
   (divides_b (i/n) (pred n)
 \land (leb (S(i\mod n)) (i/n)
 \land eqb (gcd (i\mod n) (i/n)) (S O)))
@@ -154,42 +153,8 @@ apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
   | rewrite > (NdivM_times_M_to_N )
     [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
       [ apply (monotonic_lt_times_variant (pred n)) 
-        [ apply (nat_case1 n)
-          [ intros.
-            rewrite > H2 in H:(? ? %).
-            change in H:(? ? %) with (O).
-            change in H:(%) with ((S i) \le O).
-            apply False_ind.
-            apply (not_le_Sn_O i H)  
-          | intro.
-            elim m
-            [ rewrite > H2 in H1:(%).
-              rewrite > H2 in H:(%).
-              simplify in H.
-              cut (i = O)
-              [ rewrite > Hcut in H1:(%).
-                simplify in H1.  
-                apply False_ind.  
-                apply (not_eq_true_false H1)
-              | change in H:(%) with((S i) \le (S O)).
-                cut (i \le O )
-                [ apply (nat_case1 i)
-                  [ intros.
-                    reflexivity
-                  | intros.
-                    rewrite > H3 in Hcut:(%).
-                    apply False_ind.
-                    apply (not_le_Sn_O m1 Hcut)
-                  ]
-                | apply (le_S_S_to_le i O).
-                  assumption
-                ]
-              ]
-            | change with ((S O) \le (S n1)).
-              apply (le_S_S O n1).
-              apply (le_O_n n1)
-            ]
-          ]
+        [ apply n_gt_Uno_to_O_lt_pred_n.
+          assumption      
         | change with ((S (i\mod n)) \le (i/n)).          
           apply (aux_S_i_mod_n_le_i_div_n i n);
             assumption    
@@ -221,8 +186,7 @@ apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n))
   ]
 | rewrite > (sym_times).
   rewrite > (div_times_ltO )  
-  [ apply (le_n (pred n)).
-    
+  [ apply (le_n (pred n))
   | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)).
     apply (aux_S_i_mod_n_le_i_div_n i n);
       assumption.
@@ -398,23 +362,15 @@ 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.
 
-  
-
 
 (*6th*)
 theorem sum_divisor_totient1_aux_6: \forall j,n:nat.
@@ -486,7 +442,7 @@ qed.
     
 (* The main theorem, adding the hypotesis n > 1 (the cases n= 0
    and n = 1 are dealed as particular cases in theorem 
-   sum_divisor_totiet)
+   sum_divisor_totient)
  *)        
 theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
 intros. 
@@ -611,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))