From e65e31bab82994cf8400bb4c294cf7d16fa2c83c Mon Sep 17 00:00:00 2001
From: Cristian Armentano <??>
Date: Fri, 7 Sep 2007 14:10:46 +0000
Subject: [PATCH] some simplifications.

---
 .../matita/library/nat/gcd_properties1.ma     |  55 +-----
 .../nat/propr_div_mod_lt_le_totient1_aux.ma   | 182 ++++++------------
 helm/software/matita/library/nat/totient1.ma  |  45 +----
 3 files changed, 67 insertions(+), 215 deletions(-)

diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma
index 637c20f4a..ad5cb2c6b 100644
--- a/helm/software/matita/library/nat/gcd_properties1.ma
+++ b/helm/software/matita/library/nat/gcd_properties1.ma
@@ -157,20 +157,12 @@ apply (leb_elim n m)
 ]
 qed.
 
-(* 2 basic properties of divides predicate *)
-theorem aDIVb_to_bDIVa_to_aEQb:
-\forall a,b:nat.
-a \divides b \to b \divides a \to a = b.
-intros.
-apply antisymmetric_divides;
-  assumption.
-qed.
-
+(* a basic property of divides predicate *)
 
 theorem O_div_c_to_c_eq_O: \forall c:nat.
 O \divides c \to c = O.
 intros.
-apply aDIVb_to_bDIVa_to_aEQb
+apply antisymmetric_divides
 [ apply divides_n_O
 | assumption
 ]
@@ -182,7 +174,7 @@ c \divides a \to c \divides b \to
 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
 intros.
 elim (H2 ((gcd a b)))
-[ apply (aDIVb_to_bDIVa_to_aEQb (gcd a b) c)
+[ apply (antisymmetric_divides (gcd a b) c)
   [ apply (witness (gcd a b) c n2).
     assumption
   | apply divides_d_gcd;
@@ -224,47 +216,6 @@ apply (nat_case1 c)
   ]
 ]
 qed.
-  
-  (* 
-  apply (nat_case1 a)
-  [ intros.
-    rewrite > (sym_times c O).
-    simplify.
-    reflexivity
-  | intros.
-    rewrite < H1.
-    apply (nat_case1 b)
-    [ intros.
-      rewrite > (sym_times ? O).
-      rewrite > (sym_gcd a O).
-      rewrite > sym_gcd.
-      simplify.
-      reflexivity
-    | intros.
-      rewrite < H2.
-      apply gcd1
-      [ apply divides_times
-        [ apply divides_n_n
-        | apply divides_gcd_n.
-        ]
-      | apply divides_times
-        [ apply divides_n_n
-        | rewrite > sym_gcd.  
-          apply divides_gcd_n
-        ]
-      | intros.
-        apply (divides_d_times_gcd)
-        [ rewrite > H.
-          apply lt_O_S  
-        | assumption
-        | assumption
-        ]
-      ]
-    ]
-  ]
-]
-qed.*)
-
 
 theorem associative_nat_gcd: associative nat gcd.
 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
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 fae1afc2c..975114306 100644
--- 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
@@ -112,77 +112,21 @@ apply (le_times_to_le c (a/c) a)
 qed.
 
 
-theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
-O \lt b \to (b*c) \le a \to c \le (a /b).
-intros.
-rewrite > (div_mod a b) in H1
-[ apply (le_times_to_le b ? ?)
-  [ assumption
-  | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
-    [ elim Hcut
-      [ rewrite < (sym_times c b).
-        rewrite < (sym_times (a/b) b).
-        assumption
-      | cut (a/b \lt c)
-        [ change in Hcut1 with ((S (a/b)) \le c).
-          cut( b*(S (a/b)) \le b*c)
-          [ rewrite > (sym_times b (S (a/b))) in Hcut2.
-            simplify in Hcut2.
-            cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
-            [ cut (b \le (a \mod b))
-              [ apply False_ind.
-                apply (lt_to_not_le (a \mod b) b)
-                [ apply (lt_mod_m_m).
-                  assumption
-                | assumption
-                ]
-              | apply (le_plus_to_le ((a/b)*b)).
-                rewrite > sym_plus.
-                assumption.
-              ]
-            | apply (trans_le ? (b*c) ?);
-                assumption
-            ]
-          | apply (le_times_r b ? ?).
-            assumption
-          ]
-        | apply (lt_times_n_to_lt b (a/b) c)
-          [ assumption
-          | assumption
-          ]
-        ]
-      ]
-    | apply (leb_elim (c*b) ((a/b)*b))
-      [ intros.
-        left.
-        assumption
-      | intros.
-        right.
-        apply cic:/matita/nat/orders/not_le_to_lt.con. 
-        assumption        
-      ]
-    ]
-  ]
-| assumption
-] 
-qed.
-
 theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
 \forall a,b:nat.
 O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
 intros.
 elim H2.
-cut (O \lt n2)
-[ rewrite > H3.
-  rewrite > (sym_times a n2).
-  rewrite > (div_times_ltO n2 a);
-    assumption  
-| apply (divides_to_lt_O n2 b)
+rewrite > H3.
+rewrite > (sym_times a n2).
+rewrite > (div_times_ltO n2 a)
+[ apply (divides_to_lt_O n2 b)
   [ assumption
   | apply (witness n2 b a).
     rewrite > sym_times.
     assumption
-  ] 
+  ]  
+| assumption  
 ]
 qed.
 
@@ -208,17 +152,17 @@ 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 (cic:/matita/nat/div_and_mod/inj_times_r1.con d)
+apply (inj_times_r1 d)
 [ assumption
 | rewrite > sym_times.
   rewrite < (times_n_SO d).
   assumption
 ]
-qed.
+qed.*)
 
 
 theorem div_mod_minus:
@@ -231,6 +175,7 @@ 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.
@@ -245,7 +190,7 @@ rewrite > (div_plus_times c n2 b)
 | assumption
 ]
 qed.
-
+*)
 
 (* A corollary to the division theorem (between natural numbers).
  *
@@ -270,83 +215,74 @@ split
 | rewrite < (times_n_Sm b c).
   rewrite < H1.
   rewrite > sym_times.
-  rewrite > div_mod_minus
-  [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b))
-    [ rewrite < (sym_plus a b).
-      rewrite > (eq_minus_plus_plus_minus a b (a \mod b))
-      [ rewrite > (plus_n_O a) in \vdash (? % ?).
-        apply (le_to_lt_to_plus_lt)
-        [ apply (le_n a)
-        | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con.      
-          apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con.
-          assumption
-        ]
-      | apply lt_to_le.
-        apply lt_mod_m_m.
-        assumption
-      ]
-    | rewrite > (div_mod a b) in \vdash (? ? %)
-      [ rewrite > plus_n_O in \vdash (? % ?).
-        rewrite > sym_plus.
-        apply cic:/matita/nat/le_arith/le_plus_n.con
-      | assumption
-      ]
-    ]
+  rewrite > (div_mod a b) in \vdash (? % ?)
+  [ rewrite > (sym_plus b ((a/b)*b)).
+    apply lt_plus_r.
+    apply lt_mod_m_m.
+    assumption
   | assumption
   ]
 ]
 qed.
+  
 
 theorem th_div_interi_1: \forall a,c,b:nat.
 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
 intros.
 apply (le_to_le_to_eq)
-[ cut (a/b \le c \lor c \lt a/b)
-  [ elim Hcut
-    [ assumption
-    | change in H3 with ((S c) \le (a/b)).
-      cut (b*(S c) \le (b*(a/b)))
-      [ rewrite > (sym_times b (S c)) in Hcut1.
-        cut (a \lt (b * (a/b)))
-        [ rewrite > (div_mod a b) in Hcut2:(? % ?)
-          [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %).
-            cut ((a \mod b) \lt O)
-            [ apply False_ind.
-              apply (lt_to_not_le (a \mod b) O)
-              [ assumption
-              | apply le_O_n
-              ]              
-            | apply (lt_plus_to_lt_r ((a/b)*b)).
-              rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)).
-              assumption 
-            ]
-          | assumption
-          ]
-        | apply (lt_to_le_to_lt ? (b*(S c)) ?)
+[ apply (leb_elim (a/b) c);intros
+  [ assumption
+  | cut (c \lt (a/b))
+    [ apply False_ind.
+      apply (lt_to_not_le (a \mod b) O)
+      [ apply (lt_plus_to_lt_l ((a/b)*b)).
+        simplify.
+        rewrite < sym_plus.
+        rewrite < div_mod
+        [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
           [ assumption
-          | rewrite > (sym_times b (S c)).
+          | rewrite > (sym_times (a/b) b).
+            apply le_times_r.
             assumption
           ]
+        | assumption
         ]
-      | apply le_times_r.
-        assumption
+      | apply le_O_n
       ]
-    ]
-  | apply (leb_elim (a/b) c)
-    [ intros.
-      left.
+    | apply not_le_to_lt.
       assumption
-    | intros.
-      right.
-      apply cic:/matita/nat/orders/not_le_to_lt.con. 
+    ]
+  ]
+| apply (leb_elim c (a/b));intros
+  [ assumption
+  | cut((a/b) \lt c) 
+    [ apply False_ind.
+      apply (lt_to_not_le (a \mod b) b)
+      [ apply (lt_mod_m_m).
+        assumption
+      | apply (le_plus_to_le ((a/b)*b)).
+        rewrite < (div_mod a b)
+        [ apply (trans_le ? (b*c) ?)
+          [ rewrite > (sym_times (a/b) b).
+            rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
+            rewrite < distr_times_plus.
+            rewrite > sym_plus.
+            simplify in \vdash (? (? ? %) ?).
+            apply le_times_r.
+            assumption
+          | assumption
+          ]
+        | assumption
+        ]
+      ]
+    | apply not_le_to_lt. 
       assumption
     ]
-  ] 
-| apply (bTIMESc_le_a_to_c_le_aDIVb);
-    assumption
+  ]
 ]
 qed.
 
+
 theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
 O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
 intros.
diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma
index d7483b3b4..b46120341 100644
--- a/helm/software/matita/library/nat/totient1.ma
+++ b/helm/software/matita/library/nat/totient1.ma
@@ -136,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)))
@@ -153,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    
@@ -220,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.
@@ -483,7 +448,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. 
-- 
2.39.2