]> matita.cs.unibo.it Git - helm.git/commitdiff
some theorems have been moved to more appropriate files in library.
authorCristian Armentano <??>
Tue, 18 Sep 2007 17:47:29 +0000 (17:47 +0000)
committerCristian Armentano <??>
Tue, 18 Sep 2007 17:47:29 +0000 (17:47 +0000)
helm/software/matita/library/datatypes/bool.ma
helm/software/matita/library/nat/div_and_mod.ma
helm/software/matita/library/nat/gcd_properties1.ma
helm/software/matita/library/nat/generic_iter_p.ma
helm/software/matita/library/nat/lt_arith.ma
helm/software/matita/library/nat/primes.ma
helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma [deleted file]
helm/software/matita/library/nat/totient1.ma

index b5abbb35d2b3748630fcc3faee802b9f608e7433..37a2a377d6fd39320fc8dfbdeeb1820de0fd1b25 100644 (file)
@@ -163,11 +163,10 @@ elim A;
     reflexivity.
 qed.
 
-theorem andb_t_t_t: \forall A,B,C:bool.
-A = true \to B = true \to C = true \to (A \land (B \land C)) = true.
+theorem true_to_true_to_andb_true: \forall A,B:bool.
+A = true \to B = true \to (A \land B) = true.
 intros.
 rewrite > H.
 rewrite > H1.
-rewrite > H2.
 reflexivity.
 qed.
\ No newline at end of file
index d7750e39ad7c03e4424d1d221e50710843d7e87a..658b07b686eb5e6c23f02f3247c64f02f8f25381 100644 (file)
@@ -101,6 +101,16 @@ simplify.
 apply div_aux_mod_aux.
 qed.
 
+theorem eq_times_div_minus_mod:
+\forall a,b:nat. O \lt b \to
+(a /b)*b = a - (a \mod b).
+intros.
+rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
+[ apply (minus_plus_m_m (times (div a b) b) (mod a b))
+| assumption
+]
+qed.
+
 inductive div_mod_spec (n,m,q,r:nat) : Prop \def
 div_mod_spec_intro: r < m \to n=q*m+r \to (div_mod_spec n m q r).
 
@@ -224,6 +234,15 @@ apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
 ]
 qed.
 
+(*a simple variant of div_times theorem *)
+theorem lt_O_to_div_times: \forall a,b:nat. O \lt b \to
+a*b/b = a.
+intros.
+rewrite > sym_times.
+rewrite > (S_pred b H).
+apply div_times.
+qed.
+
 theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
 intros.
 apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O).
@@ -333,13 +352,3 @@ let rec n_divides_aux p n m acc \def
 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
 
-
-(*a simple variant of div_times theorem *)
-theorem div_times_ltO: \forall a,b:nat. O \lt b \to
-a*b/b = a.
-intros.
-rewrite > sym_times.
-rewrite > (S_pred b H).
-apply div_times.
-qed.
-
index 535e7b42a25cc5a05f4df39f4394a69db9fa8e00..8687e2c1f7ececee716b5fdcf0efc1136e3b9313 100644 (file)
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/gcd_properties1".
 
-include "nat/propr_div_mod_lt_le_totient1_aux.ma".
+include "nat/gcd.ma".
 
 (* this file contains some important properites of gcd in N *)
 
@@ -238,107 +238,96 @@ apply gcd1
 ]
 qed.
 
-theorem divides_times_to_gcd_to_divides_div: \forall a,b,c,d:nat.
-a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
+
+theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
+O \lt m \to m \divides a \to m \divides b \to 
+(gcd (a/m) (b/m)) = (gcd a b) / m.
+intros.
+apply (inj_times_r1 m H).
+rewrite > (sym_times m ((gcd a b)/m)).
+rewrite > (divides_to_times_div (gcd a b) m)
+[ rewrite < eq_gcd_times_times_times_gcd.
+  rewrite > (sym_times m (a/m)).
+  rewrite > (sym_times m (b/m)).
+  rewrite > (divides_to_times_div a m H H1).
+  rewrite > (divides_to_times_div b m H H2).
+  reflexivity
+| assumption
+| apply divides_d_gcd;
+    assumption
+]
+qed.
+
+
+
+theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat.
+a \divides (b*c) \to (a/(gcd a b)) \divides c.
 intros.
 apply (nat_case1 a)
 [ intros.
   apply (nat_case1 b)
-  [ intros.
-    cut (d = O) (*this is an impossible case*)
+  [ (*It's an impossible situation*)
+    intros. 
+    simplify.
+    apply divides_SO_n
+  | intros.    
+    cut (c = O)
     [ rewrite > Hcut.
-      simplify.
-      apply divides_SO_n
-    | rewrite > H2 in H1.
-      rewrite > H3 in H1.
-      apply sym_eq.
-      assumption
-    ]
-  | intros.
-    cut (O \lt d)
-    [ rewrite > (S_pred d Hcut).
-      simplify.
-      rewrite > H2 in H.
-      cut (c = O)
-      [ rewrite > Hcut1.
-        apply (divides_n_n O)
-      | apply (lt_times_eq_O b c)
-        [ rewrite > H3.
-          apply lt_O_S
-        | apply antisymmetric_divides
-          [ apply divides_n_O
-          | assumption
-          ]
+      apply (divides_n_n O)
+    | apply (lt_times_eq_O b c)
+      [ rewrite > H2.
+        apply lt_O_S
+      | apply antisymmetric_divides
+        [ apply divides_n_O
+        | rewrite < H1.
+          assumption
         ]
       ]
-    | rewrite < H1.
-      apply lt_O_gcd.
-      rewrite > H3.
-      apply lt_O_S
     ]
   ]
 | intros.
-  rewrite < H2.
+  rewrite < H1.
   elim H.
-  cut (d \divides a \land d \divides b)
-  [ cut (O \lt a)
-    [ cut (O \lt d)
-      [ elim Hcut.
-        rewrite < (NdivM_times_M_to_N a d) in H3
-        [ rewrite < (NdivM_times_M_to_N b d) in H3 
-          [ cut (b/d*c = a/d*n2)
-            [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
-              [ apply (O_lt_times_to_O_lt (a/d) d).
-                rewrite > (NdivM_times_M_to_N a d);
-                  assumption
-              | apply (inj_times_r1 d ? ?)
-                [ assumption
-                | rewrite < (eq_gcd_times_times_times_gcd (a/d) (b/d) d).
-                  rewrite < (times_n_SO d).
-                  rewrite < (sym_times (a/d) d).
-                  rewrite < (sym_times (b/d) d).
-                  rewrite > (NdivM_times_M_to_N a d)
-                  [ rewrite > (NdivM_times_M_to_N b d);
-                      assumption                    
-                  | assumption
-                  | assumption              
-                  ]
-                ]
-              | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
-              ]
-            | apply (inj_times_r1 d ? ?)
-              [ assumption
-              | rewrite > sym_times.
-                rewrite > (sym_times d ((a/d) * n2)).
-                rewrite > assoc_times.
-                rewrite > (assoc_times (a/d) n2 d).            
-                rewrite > (sym_times c d).
-                rewrite > (sym_times n2 d).              
-                rewrite < assoc_times.
-                rewrite < (assoc_times (a/d) d n2).
-                assumption
-              ]
-            ]
-          | assumption
+  cut (O \lt a)
+  [ cut (O \lt (gcd a b))
+    [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
+      [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
+        rewrite > (divides_to_times_div a (gcd a b))
+        [ assumption      
+        | assumption
+        | apply divides_gcd_n
+        ]
+      | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
+        [ apply eq_gcd_div_div_div_gcd
+          [ assumption
+          | apply divides_gcd_n
+          | apply divides_gcd_m
+          ]
+        | assumption
+        ]
+      | apply (witness ? ? n2).
+        apply (inj_times_r1 (gcd a b) Hcut1).
+        rewrite < assoc_times.
+        rewrite < sym_times in \vdash (? ? (? % ?) ?).
+        rewrite > (divides_to_times_div b (gcd a b))
+        [ rewrite < assoc_times in \vdash (? ? ? %).
+          rewrite < sym_times in \vdash (? ? ? (? % ?)).
+          rewrite > (divides_to_times_div a (gcd a b))
+          [ assumption
           | assumption
+          | apply divides_gcd_n
           ]
         | assumption
-        | assumption    
+        | apply divides_gcd_m
         ]
-      | rewrite < H1.
-        rewrite > sym_gcd.
-        apply lt_O_gcd.
-        assumption
       ]
-    | rewrite > H2.
-      apply lt_O_S
-    ]
-  | rewrite < H1.
-    split
-    [ apply divides_gcd_n
-    | apply divides_gcd_m
+    | rewrite > sym_gcd.
+      apply lt_O_gcd.
+      assumption    
     ]
-  ]
+  | rewrite > H1.
+    apply lt_O_S
+  ]    
 ]
 qed.
 
@@ -374,53 +363,14 @@ apply gcd1
 qed.
 
 
-theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
-O \lt m \to m \divides a \to m \divides b \to 
-(gcd (a/m) (b/m)) = (gcd a b) / m.
-intros.
-apply (inj_times_r1 m H).
-rewrite > (sym_times m ((gcd a b)/m)).
-rewrite > (NdivM_times_M_to_N (gcd a b) m)
-[ rewrite < eq_gcd_times_times_times_gcd.
-  rewrite > (sym_times m (a/m)).
-  rewrite > (sym_times m (b/m)).
-  rewrite > (NdivM_times_M_to_N a m H H1).
-  rewrite > (NdivM_times_M_to_N b m H H2).
-  reflexivity
-| assumption
-| apply divides_d_gcd;
-    assumption
-]
-qed.
-
 
 theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat.
 (gcd e f) = (S O)  \to e \divides c \to f \divides c \to 
 (e*f) \divides c.
 intros.
-apply (nat_case1 e)
-[ intros.
-  apply (nat_case1 c)
-  [ intros.
-    simplify.
-    apply (divides_n_n O).
-  | intros.
-    rewrite > H3 in H1.
-    apply False_ind.
-    cut (O \lt O)
-    [ apply (le_to_not_lt O O)
-      [ apply (le_n O)
-      | assumption
-      ]
-    | apply (divides_to_lt_O O c)
-      [ rewrite > H4.
-        apply lt_O_S
-      | assumption
-      ]
-    ]
-  ]
-| intros.
-  rewrite < H3.
+apply (nat_case1 c); intros
+[ apply divides_n_O 
+| rewrite < H3.
   elim H1.
   elim H2.
   rewrite > H5.
@@ -429,16 +379,18 @@ apply (nat_case1 e)
   [ apply (divides_n_n)
   | rewrite > H5 in H1.
     apply (gcd_SO_to_divides_times_to_divides f e n)
-    [ rewrite > H3.
-      apply (lt_O_S m)
+    [ rewrite < H5 in H1.
+      rewrite > H3 in H1.
+      apply (divides_to_lt_O e (S m))
+      [ apply lt_O_S
+      | assumption
+      ]
     | assumption
     | assumption
     ]
   ]
 ]
 qed.
-
-
 (* the following theorem shows that gcd is a multiplicative function in 
    the following sense: if a1 and a2 are relatively prime, then 
    gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b). 
index 75100b3f5b0e0cba6b66863d6377704c3bcce9ac..c424f82e0318064b1a31ee6c406d4f8b55089327 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/generic_iter_p.ma".
+set "baseuri" "cic:/matita/nat/generic_iter_p".
 
 include "nat/primes.ma".
 include "nat/ord.ma".
index e7151472610319dd7a69c2e15ead3e3104f40d6c..cce6626a0f43d9273c23a2be0ea6fa90fd55a105 100644 (file)
@@ -301,6 +301,162 @@ unfold lt. apply le_n.assumption.
 qed.
 
 
+(* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
+(* The theorem is shown in two different parts: *)
+
+theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
+O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
+intros.
+split
+[ rewrite < H1.
+  rewrite > sym_times.
+  rewrite > eq_times_div_minus_mod
+  [ apply (le_minus_m a (a \mod b))
+  | assumption
+  ]
+| rewrite < (times_n_Sm b c).
+  rewrite < H1.
+  rewrite > sym_times.
+  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 lt_to_le_times_to_lt_S_to_div: \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)
+[ 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 (a/b) b).
+            apply le_times_r.
+            assumption
+          ]
+        | assumption
+        ]
+      | apply le_O_n
+      ]
+    | apply not_le_to_lt.
+      assumption
+    ]
+  ]
+| 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
+    ]
+  ]
+]
+qed.
+
+
+theorem lt_to_lt_to_eq_div_div_times_times: \forall a,b,c:nat. 
+O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
+intros.
+apply sym_eq.
+cut (b*(a/b) \le a \land a \lt b*(S (a/b)))
+[ elim Hcut.
+  apply lt_to_le_times_to_lt_S_to_div
+  [ rewrite > (S_pred b)
+    [ rewrite > (S_pred c)
+      [ apply (lt_O_times_S_S)
+      | assumption
+      ]
+    | assumption
+    ]
+  | rewrite > assoc_times.
+    rewrite > (sym_times c (a/b)).
+    rewrite < assoc_times.
+    rewrite > (sym_times (b*(a/b)) c).
+    rewrite > (sym_times a c).
+    apply (le_times_r c (b*(a/b)) a).
+    assumption
+  | rewrite > (sym_times a c).
+    rewrite > (assoc_times ).
+    rewrite > (sym_times c (S (a/b))).
+    rewrite < (assoc_times).
+    rewrite > (sym_times (b*(S (a/b))) c).
+    apply (lt_times_r1 c a (b*(S (a/b))));
+      assumption    
+  ]
+| apply (lt_to_div_to_and_le_times_lt_S)
+  [ assumption
+  | reflexivity
+  ]
+]
+qed.
+
+theorem times_mod: \forall a,b,c:nat.
+O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
+intros.
+apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
+[ rewrite > (lt_to_lt_to_eq_div_div_times_times a b c)
+  [ apply div_mod_spec_div_mod.
+    rewrite > (S_pred b)
+    [ rewrite > (S_pred c)
+      [ apply lt_O_times_S_S
+      | assumption
+      ]
+    | assumption
+    ]
+  | assumption
+  | assumption
+  ]
+| apply div_mod_spec_intro
+  [ rewrite > (sym_times b c).
+    apply (lt_times_r1 c)
+    [ assumption
+    | apply (lt_mod_m_m).
+      assumption
+    ]
+  | rewrite < (assoc_times (a/b) b c).
+    rewrite > (sym_times a c).
+    rewrite > (sym_times ((a/b)*b) c).
+    rewrite < (distr_times_plus c ? ?).
+    apply eq_f.
+    apply (div_mod a b).
+    assumption
+  ]
+]
+qed.
+
+
+
+
 (* general properties of functions *)
 theorem monotonic_to_injective: \forall f:nat\to nat.
 monotonic nat lt f \to injective nat nat f.
@@ -322,3 +478,4 @@ increasing f \to injective nat nat f.
 intros.apply monotonic_to_injective.
 apply increasing_to_monotonic.assumption.
 qed.
+
index a95b2e88fddda2344f0fafc448593de57404d470..45f520d087115bb5c5b7c105e569e6f2ce2efe1d 100644 (file)
@@ -190,6 +190,45 @@ rewrite > H2.rewrite < H3.
 simplify.exact (not_le_Sn_n O).
 qed.
 
+(*divides and div*)
+
+theorem divides_to_times_div: \forall n,m:nat.
+O \lt m \to m \divides n \to (n / m) * m = n.
+intros.
+rewrite > plus_n_O.
+apply sym_eq.
+cut (n \mod m = O)
+[ rewrite < Hcut.
+  apply div_mod.
+  assumption
+| apply divides_to_mod_O;
+    assumption.
+]
+qed.
+
+(*to remove hypotesis b > 0*)
+theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat.
+O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
+(*theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat.
+c \divides b \to a * (b /c) = (a*b)/c.*)
+intros.
+elim H1.
+rewrite > H2.
+rewrite > (sym_times c n2).
+cut(O \lt c)
+[ rewrite > (lt_O_to_div_times n2 c)
+  [ rewrite < assoc_times.
+    rewrite > (lt_O_to_div_times (a *n2) c)
+    [ reflexivity
+    | assumption
+    ]
+  | assumption
+  ]  
+| apply (divides_to_lt_O c b);
+    assumption.
+]
+qed.
+
 (* boolean divides *)
 definition divides_b : nat \to nat \to bool \def
 \lambda n,m :nat. (eqb (m \mod n) O).
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
deleted file mode 100644 (file)
index f26f0ea..0000000
+++ /dev/null
@@ -1,358 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/".
-
-include "nat/iteration2.ma".
-
-(*this part of the library contains some properties useful to prove
-  the main theorem in totient1.ma, and some new properties about gcd
-  (see gcd_properties1.ma).
-  These theorems are saved separately from the other part of the library
-  in order to avoid to create circular dependences in it.
- *)
-
-(* some basic properties of and - or*)
-(*theorem andb_sym: \forall A,B:bool.
-(A \land B) = (B \land A).
-intros.
-elim A;
-  elim B;
-    simplify;
-    reflexivity.
-qed.
-
-theorem andb_assoc: \forall A,B,C:bool.
-(A \land (B \land C)) = ((A \land B) \land C).
-intros.
-elim A;
-  elim B;
-    elim C;
-      simplify;
-      reflexivity.
-qed.
-
-theorem orb_sym: \forall A,B:bool.
-(A \lor B) = (B \lor A).
-intros.
-elim A;
-  elim B;
-    simplify;
-    reflexivity.
-qed.
-
-theorem andb_t_t_t: \forall A,B,C:bool.
-A = true \to B = true \to C = true \to (A \land (B \land C)) = true.
-intros.
-rewrite > H.
-rewrite > H1.
-rewrite > H2.
-reflexivity.
-qed.
-*)
-(*properties about relational operators*)
-
-theorem Sa_le_b_to_O_lt_b: \forall a,b:nat.
-(S a) \le b \to O \lt b.
-intros.
-elim H;
-  apply lt_O_S.
-qed.
-
-
-theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
-(S O) \lt n \to O \lt (pred n).
-intros.
-apply (Sa_le_b_to_O_lt_b (pred (S O)) (pred n) ?).
- apply (lt_pred (S O) n ? ?);
- [ apply (lt_O_S O) 
- | apply (H)
- ]
-qed.
-
-
-theorem NdivM_times_M_to_N: \forall n,m:nat.
-O \lt m \to m \divides n \to (n / m) * m = n.
-intros.
-rewrite > plus_n_O.
-apply sym_eq.
-cut (n \mod m = O)
-[ rewrite < Hcut.
-  apply div_mod.
-  assumption
-| apply divides_to_mod_O;
-    assumption.
-]
-qed.
-
-theorem lt_to_divides_to_div_le:  \forall a,c:nat.
-O \lt c \to c \divides a \to a/c \le a.
-intros.
-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 (? % ?)
-  [ apply (le_times_n c a ?).   
-    assumption
-  | 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.
-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.
-
-(* some properties of div operator between natural numbers *)
-
-theorem separazioneFattoriSuDivisione: \forall a,b,c:nat.
-O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
-intros.
-elim H1.
-rewrite > H2.
-rewrite > (sym_times c n2).
-cut(O \lt c)
-[ rewrite > (div_times_ltO n2 c)
-  [ rewrite < assoc_times.
-    rewrite > (div_times_ltO (a *n2) c)
-    [ reflexivity
-    | assumption
-    ]
-  | assumption
-  ]  
-| apply (divides_to_lt_O c b);
-    assumption.
-]
-qed.
-
-
-theorem div_mod_minus:
-\forall a,b:nat. O \lt b \to
-(a /b)*b = a - (a \mod b).
-intros.
-rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
-[ apply (minus_plus_m_m (times (div a b) b) (mod a b))
-| assumption
-]
-qed.
-
-
-(* A corollary to the division theorem (between natural numbers).
- *
- * Forall a,b,c: Nat, b > O,
- *  a/b = c iff (b*c <= a && a < b*(c+1)
- *
- * two parts of the theorem are proved separately
- *  - (=>) th_div_interi_2
- *  - (<=) th_div_interi_1
- *)
-
-theorem th_div_interi_2: \forall a,b,c:nat.
-O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
-intros.
-split
-[ rewrite < H1.
-  rewrite > sym_times.
-  rewrite > div_mod_minus
-  [ apply (le_minus_m a (a \mod b))
-  | assumption
-  ]
-| rewrite < (times_n_Sm b c).
-  rewrite < H1.
-  rewrite > sym_times.
-  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)
-[ 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 (a/b) b).
-            apply le_times_r.
-            assumption
-          ]
-        | assumption
-        ]
-      | apply le_O_n
-      ]
-    | apply not_le_to_lt.
-      assumption
-    ]
-  ]
-| 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
-    ]
-  ]
-]
-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.
-apply sym_eq.
-cut (b*d \le a \land a \lt b*(S d))
-[ elim Hcut.
-  apply th_div_interi_1
-  [ rewrite > (S_pred b)
-    [ rewrite > (S_pred c)
-      [ apply (lt_O_times_S_S)
-      | assumption
-      ]
-    | assumption
-    ]
-  | rewrite > assoc_times.
-    rewrite > (sym_times c d).
-    rewrite < assoc_times.
-    rewrite > (sym_times (b*d) c).
-    rewrite > (sym_times a c).
-    apply (le_times_r c (b*d) a).
-    assumption
-  | rewrite > (sym_times a c).
-    rewrite > (assoc_times ).
-    rewrite > (sym_times c (S d)).
-    rewrite < (assoc_times).
-    rewrite > (sym_times (b*(S d)) c).
-    apply (lt_times_r1 c a (b*(S d)));
-      assumption    
-  ]
-| apply (th_div_interi_2)
-  [ assumption
-  | apply sym_eq.
-    assumption
-  ]
-]
-qed.
-
-theorem times_numerator_denominator: \forall a,b,c:nat. 
-O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
-intros.
-apply (times_numerator_denominator_aux a b c (a/b))
-[ assumption
-| assumption
-| reflexivity
-]
-qed.
-
-theorem times_mod: \forall a,b,c:nat.
-O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
-intros.
-apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
-[ apply div_mod_spec_intro
-  [ apply (lt_mod_m_m (a*c) (b*c)).
-    rewrite > (S_pred b)
-    [ rewrite > (S_pred c)
-      [ apply lt_O_times_S_S
-      | assumption
-      ]
-    | assumption
-    ]
-  | rewrite > (times_numerator_denominator a b c)
-    [ apply (div_mod (a*c) (b*c)).
-      rewrite > (S_pred b)
-      [ rewrite > (S_pred c)
-        [ apply (lt_O_times_S_S)
-        | assumption
-        ]
-      | assumption
-      ]
-    | assumption
-    | assumption
-    ]
-  ]
-| constructor 1
-  [ rewrite > (sym_times b c).
-    apply (lt_times_r1 c)
-    [ assumption
-    | apply (lt_mod_m_m).
-      assumption
-    ]
-  | rewrite < (assoc_times (a/b) b c).
-    rewrite > (sym_times a c).
-    rewrite > (sym_times ((a/b)*b) c).
-    rewrite < (distr_times_plus c ? ?).
-    apply eq_f.
-    apply (div_mod a b).
-    assumption
-  ]
-]
-qed.
-
-
-
-
-
-
-
-
-
-
-
index 5ce43d4ac0c968e8006ffb2c5685864fca904321..3d6b6fafcfbc1b5817732e3b2d09702b86ee250b 100644 (file)
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/nat/totient1".
 
 include "nat/totient.ma".
 include "nat/iteration2.ma".
-include "nat/propr_div_mod_lt_le_totient1_aux.ma".
 include "nat/gcd_properties1.ma".
 
 (* This file contains the proof of the following theorem about Euler's totient
@@ -25,686 +24,248 @@ include "nat/gcd_properties1.ma".
    The sum of the applications of Phi function over the divisor of a natural
    number n is equal to n
  *)
-  
-(*two easy properties of gcd, directly obtainable from the more general theorem 
-  eq_gcd_times_times_eqv_times_gcd*)
 
-theorem gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO:\forall a,b,d:nat.
-O \lt d \to O \lt b \to gcd (b*d) (a*d) = d \to (gcd a b) = (S O).
+theorem eq_div_times_div_times: \forall a,b,c:nat.
+O \lt b \to b \divides a \to b \divides c \to
+a / b * c = a * (c/b).
 intros.
-apply (inj_times_r1 d)
-[ assumption
-| rewrite < (times_n_SO d).
-  rewrite < (eq_gcd_times_times_eqv_times_gcd a b d).
-  rewrite > sym_gcd.
-  rewrite > (sym_times d a).
-  rewrite > (sym_times d b).
-  assumption
-]
-qed.
-
-theorem gcd_SO_to_gcd_times: \forall a,b,c:nat.
-O \lt c \to (gcd a b) = (S O) \to (gcd (a*c) (b*c)) = c.
-intros.
-rewrite > (sym_times a c).
-rewrite > (sym_times b c).
-rewrite > (eq_gcd_times_times_eqv_times_gcd a b c).
-rewrite > H1.
-apply sym_eq.
-apply times_n_SO.
+elim H1.
+elim H2.
+rewrite > H3.
+rewrite > H4.    
+rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))).
+rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?).
+rewrite > (lt_O_to_div_times ? ? H).
+rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)).
+rewrite > (sym_times b n2).
+rewrite > assoc_times.
+reflexivity.
 qed.
-
-
-(* The proofs of the 6 sub-goals activated after the application of the theorem 
-   eq_sigma_p_gh in the proof of the main theorem
- *)
-
-
-(* 2nd*)
-theorem sum_divisor_totient1_aux2: \forall i,n:nat.
-(S O) \lt n \to i<n*n \to 
-  (i/n) \divides (pred n) \to
-  (i \mod n) \lt (i/n) \to
-  (gcd (i \mod n) (i/n)) = (S O) \to
-     gcd (pred n) ((i\mod n)* (pred n)/(i/n)) = (pred n) / (i/n).             
+    
+theorem lt_O_to_divides_to_lt_O_div:
+\forall a,b:nat.
+O \lt b \to a \divides b \to O \lt (b/a).
 intros.
-cut (O \lt (pred n))
-[ cut(O \lt (i/n))
-  [ rewrite < (NdivM_times_M_to_N (pred n) (i/n)) in \vdash (? ? (? % ?) ?)
-    [ rewrite > (sym_times ((pred n)/(i/n)) (i/n)).
-      cut ((i \mod n)*(pred n)/(i/n) = (i \mod n) * ((pred n) / (i/n)))
-      [ rewrite > Hcut2.
-        apply (gcd_SO_to_gcd_times (i/n) (i \mod n) ((pred n)/(i/n)))
-        [ apply (lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb (i/n) (pred n));
-            assumption
-        | rewrite > sym_gcd.
-          assumption            
-        ]
-      | apply sym_eq.
-        apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n));
-          assumption.
-      ]           
-    | assumption
-    | assumption
-    ]
-  | apply (divides_to_lt_O (i/n) (pred n));
-      assumption
-  ]        
-| apply n_gt_Uno_to_O_lt_pred_n.
-  assumption.
-]
-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
-            (leb (S(i\mod n)) (i/n) \land
-            eqb (gcd (i\mod n) (i/n)) (S O))) =true         
-         \to
-         (S (i\mod n)) \le (i/n).
-intros.         
-cut (leb (S (i \mod n)) (i/n) = true)
-[ change with (
-  match (true) with
-  [ true  \Rightarrow (S (i \mod n)) \leq (i/n) 
-  | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
-  ).
-  rewrite < Hcut.  
-  apply (leb_to_Prop (S(i \mod n)) (i/n))
-| apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n))  ).
-  apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
-    (eqb (gcd (i\mod n) (i/n)) (S O))
-  ).
-  rewrite > andb_sym in \vdash (? ? (? % ?) ?).
-  rewrite < (andb_assoc) in \vdash (? ? % ?).
-  assumption
+apply (O_lt_times_to_O_lt ? a).
+rewrite > (divides_to_times_div b a)
+[ assumption
+| apply (divides_to_lt_O a b H H1)
+| assumption
 ]
 qed.
 
-
-(*the following theorem is just a particular case of the theorem
-  divides_times, prooved in primes.ma
- *)
-theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat.
-a \divides b \to a \divides (b*c).
-intros.
-rewrite > (times_n_SO a).
-apply (divides_times).
-assumption.
-apply divides_SO_n.
-qed.
-
-theorem sum_divisor_totient1_aux_3: \forall i,n:nat.
-(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)))
-       =true
-   \to i\mod n*pred n/(i/n)<(pred n).
-intros.
-apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n)) 
-                ((i/n)*(pred n) / (i/n))
-                 (pred n))               
-[ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/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.  
-  | rewrite > (NdivM_times_M_to_N )
-    [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %)
-      [ apply (monotonic_lt_times_variant (pred n)) 
-        [ 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    
-        ]
-      | 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);
+(*tha main theorem*) 
+theorem sigma_p_Sn_divides_b_totient_n': \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
+intros. 
+unfold totient.
+apply (trans_eq ? ? 
+(sigma_p (S n) (\lambda d:nat.divides_b d n)
+(\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
+[ apply eq_sigma_p1
+  [ intros.
+    reflexivity
+  | intros.
+    apply sym_eq.
+    apply (trans_eq ? ? 
+     (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
+    [ apply false_to_eq_sigma_p
+      [ apply lt_to_le.          
+        assumption
+      | intros.
+        rewrite > lt_to_leb_false
+        [ reflexivity
+        | apply le_S_S.
           assumption
-      | rewrite > (times_n_SO (i/n)) in \vdash (? % ?).
-        apply (divides_times).
-        apply divides_n_n.  
-        apply divides_SO_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
-    | rewrite > (times_n_SO (i/n)).
-      rewrite > (sym_times (i \mod n) (pred n)).
-      apply (divides_times)
-      [ apply divides_b_true_to_divides.
-        apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))). 
-        apply (andb_true_true 
-            ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)))  
-            (eqb (gcd (i\mod n) (i/n)) (S O))).
-        rewrite < (andb_assoc) in \vdash (? ? % ?).
-        assumption
-      | apply divides_SO_n
+    | apply eq_sigma_p
+      [ intros.
+        rewrite > le_to_leb_true
+        [ reflexivity
+        | assumption
+        ]
+      | intros.
+        reflexivity
       ]
     ]
   ]
-| rewrite > (sym_times).
-  rewrite > (div_times_ltO )  
-  [ 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.
-  ]    
-]qed.
-
-
-(*4th*)
-theorem sum_divisor_totient1_aux_4: \forall j,n:nat.
-j \lt (pred n) \to (S O) \lt n \to
-((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n))
- \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n))
-        ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n))
-        \land (eqb
-              (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)
-               ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O))))
-=true.
-intros.
-cut (O \lt (pred n))
-[ cut ( O \lt (gcd (pred n) j))
-  [ cut (j/(gcd (pred n) j) \lt n)
-    [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j)
-      [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j)
-        [ rewrite > Hcut3.
-          rewrite > Hcut4.
-          apply andb_t_t_t
-          [ apply divides_to_divides_b_true
-            [ apply (lt_times_n_to_lt  (gcd (pred n) j) O (pred n/gcd (pred n) j))
-              [ assumption
-              | rewrite > (sym_times O (gcd (pred n) j)).
-                rewrite < (times_n_O (gcd (pred n) j)).
-                rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+| apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
+  [ apply sym_eq.
+    apply (sigma_p_knm
+     (\lambda x. (S O))
+     (\lambda i,j.j*(n/i))
+     (\lambda p. n / (gcd p n))
+     (\lambda p. p / (gcd p n))
+    );intros
+    [ cut (O \lt (gcd x n))
+      [split
+      [ split
+        [ split
+          [ split
+            [ apply divides_to_divides_b_true
+              [ apply (O_lt_times_to_O_lt ? (gcd x n)).
+                rewrite > (divides_to_times_div n (gcd x n))
                 [ assumption
                 | assumption
-                | apply (divides_gcd_n (pred n))
+                | apply (divides_gcd_m)
                 ]
+              | rewrite > sym_gcd.
+                apply (divides_times_to_divides_div_gcd).
+                apply (witness n (x * n) x).
+                apply (symmetric_times x n)
               ]
-            | apply (witness (pred n/(gcd (pred n) j))  (pred n) (gcd (pred n) j)).
-              rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
-              [ reflexivity
-              | assumption
-              | apply (divides_gcd_n (pred n))
-              ]
-            ]
-          | apply (le_to_leb_true).
-            apply lt_S_to_le.
-            apply cic:/matita/algebra/finite_groups/lt_S_S.con.
-            apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
-            [ assumption
-            | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
-              [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j))
+            | apply (true_to_true_to_andb_true)
+              [ apply (le_to_leb_true).
+                change with (x/(gcd x n) \lt n/(gcd x n)).
+                apply (lt_times_n_to_lt (gcd x n) ? ?)
                 [ assumption
+                | rewrite > (divides_to_times_div x (gcd x n))
+                  [ rewrite > (divides_to_times_div n (gcd x n))
+                    [ assumption
+                    | assumption
+                    | apply divides_gcd_m
+                    ]
+                  | assumption
+                  | apply divides_gcd_n
+                  ]
+                ]
+              | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
+                rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
+                [ apply (div_n_n (gcd x n) Hcut)
                 | assumption
                 | apply divides_gcd_n
+                | apply divides_gcd_m                  
                 ]
-              | assumption
-              | rewrite > sym_gcd.
-                apply divides_gcd_n
               ]
-            ]
-          | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
-            apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j))
-            [ assumption
-            | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
+            ] 
+          | apply (inj_times_l1 (n/(gcd x n)))
+            [ apply lt_O_to_divides_to_lt_O_div
               [ assumption
-              | simplify.
-                rewrite > NdivM_times_M_to_N
+              | apply divides_gcd_m 
+              ]
+            | rewrite > associative_times.
+              rewrite > (divides_to_times_div n (n/(gcd x n)))
+              [ apply eq_div_times_div_times
                 [ assumption
-                | assumption
                 | apply divides_gcd_n
+                | apply divides_gcd_m
                 ]
-              ]
-            | rewrite > NdivM_times_M_to_N
-              [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j))
-                [ reflexivity            
-                | assumption
-                | rewrite > sym_gcd.
-                  apply divides_gcd_n
-                ]            
-              | assumption
-              | apply divides_gcd_n
-              ]
-            ]
-          ]
-        | apply (mod_plus_times).
-          assumption
-        ]
-      | apply (div_plus_times).
-        assumption
-      ]
-    | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?)
-      [ assumption
-      | rewrite > NdivM_times_M_to_N
-        [ apply (lt_to_le_to_lt j (pred n) ?)
-          [ assumption
-          | apply (lt_to_le).
-            apply (lt_to_le_to_lt ? n ?)
-            [ change with ((S (pred n)) \le n).
-              rewrite < (S_pred n)
-              [ apply le_n
-              | apply (trans_lt ? (S O)  ?)
-                [ change with ((S O) \le (S O)).
-                  apply (le_n (S O))
+                (*rewrite > sym_times.
+                rewrite > (divides_to_eq_times_div_div_times n).
+                rewrite > (divides_to_eq_times_div_div_times x).
+                rewrite > (sym_times n x).
+                reflexivity. 
+                assumption.
+                apply divides_gcd_m.
+                apply (divides_to_lt_O (gcd x n)).
+                apply lt_O_gcd.
+                assumption.                
+                apply divides_gcd_n.*)
+              | apply lt_O_to_divides_to_lt_O_div
+                [ assumption
+                | apply divides_gcd_m 
+                ] 
+              | apply (witness ? ? (gcd x n)).
+                rewrite > divides_to_times_div
+                [ reflexivity
                 | assumption
+                | apply divides_gcd_m
+                
                 ]                
               ]
-            | rewrite > (times_n_SO n) in \vdash (? % ?).
-              apply (le_times n)
-              [ apply (le_n n)
-              | change with (O \lt (gcd (pred n) j)).
-                assumption
-              ]
-            ]
+            ]  
           ]
-        | assumption
-        | rewrite > sym_gcd.
-          apply (divides_gcd_n)
-        ]
-      ]
-    ]
-  | rewrite > sym_gcd.
-    apply (lt_O_gcd).
-    assumption
-  ]
-| apply n_gt_Uno_to_O_lt_pred_n.
-  assumption
-]
-qed.
-
-
-
-
-(*5th*)
-theorem sum_divisor_totient1_aux5: \forall a,b,c:nat.
-O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to
-a / b * c / (c/b) = a.
-intros.
-elim H3.
-elim H4.
-cut (O \lt n)
-[ rewrite > H6 in \vdash (? ? (? ? %) ?).
-  rewrite > sym_times in \vdash (? ? (? ? %) ?).
-  rewrite > (div_times_ltO n b)
-  [ cut (n \divides c)
-    [ cut (a/b * c /n = a/b * (c/n))
-      [ rewrite > Hcut2.
-        cut (c/n = b)
-        [ rewrite > Hcut3.
-          apply (NdivM_times_M_to_N a b);
+        | apply (le_to_lt_to_lt ? n)
+          [ apply cic:/matita/Z/dirichlet_product/le_div.con.
             assumption
-        | rewrite > H6.
-          apply (div_times_ltO b n).
-          assumption
-        ]
-      | elim Hcut1.
-        rewrite > H7.
-        rewrite < assoc_times in \vdash (? ? (? % ?) ?).
-        rewrite > (sym_times ((a/b)*n) n1).
-        rewrite < (assoc_times n1 (a/b) n).
-        rewrite > (div_times_ltO (n1*(a/b)) n)
-        [ rewrite > (sym_times n n1).
-          rewrite > (div_times_ltO n1 n)
-          [ rewrite > (sym_times (a/b) n1).
-            reflexivity
-          | assumption
+          | change with ((S n) \le (S n)).
+            apply le_n 
           ]
-        | assumption
         ]
-      ]
-    | apply (witness n c b).
-      rewrite > (sym_times n b).
-      assumption
-    ]
-  | assumption
-  ]
-| 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.
-j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j)<n*n.
-intros.
-apply (nat_case1 n)
-[ intros.
-  rewrite > H2 in H.
-  apply False_ind.
-  apply (not_le_Sn_O j H)
-| intros.
-  rewrite < (pred_Sn m).
-  rewrite < (times_n_Sm (S m) m).
-  rewrite > (sym_plus (S m) ((S m) * m)).
-  apply le_to_lt_to_plus_lt
-  [ rewrite > (sym_times (S m) m).
-    apply le_times_l.
-    apply (lt_to_divides_to_div_le)
-    [ apply (nat_case1 m)
-      [ intros.
-        rewrite > H3 in H2.
-        rewrite > H2 in H1.
-        apply False_ind.
-        apply (le_to_not_lt (S O) (S O))
-        [ apply le_n
-        | assumption
-        ]
-      | intros.
-        rewrite > sym_gcd in \vdash (? ? %).
-        apply (lt_O_gcd j (S m1)).
-        apply (lt_O_S m1)       
-      ]
-    | apply divides_gcd_n
-    ]
-  | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m))
-    [
-      apply lt_to_divides_to_div_le
-      [ apply (nat_case1 m)
-        [ intros.
-          rewrite > H3 in H2.
-          rewrite > H2 in H1.
-          apply False_ind.
-          apply (le_to_not_lt (S O) (S O))
-          [ apply le_n
-          | assumption
+      | apply (le_to_lt_to_lt ? x)
+        [ apply cic:/matita/Z/dirichlet_product/le_div.con.
+          assumption   
+        | apply (trans_lt ? n ?)
+          [ assumption
+          | change with ((S n) \le (S n)).
+            apply le_n
           ]
-        | intros.
-          rewrite > sym_gcd in \vdash (? ? %).
-          apply (lt_O_gcd j (S m1)).
-          apply (lt_O_S m1)
         ]
-      | rewrite > sym_gcd in \vdash (? % ?).
-        apply divides_gcd_n
-      ]
-    | rewrite > H2 in H.
-      rewrite < (pred_Sn m) in H.
-      apply (trans_lt j m (S m))
-      [ assumption.
-      | change with ((S m) \le (S m)).
-        apply (le_n (S m)) 
       ]
-    ]
-  ]
-]
-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_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. 
-unfold totient.
-apply (trans_eq ? ? 
-(sigma_p n (\lambda d:nat.divides_b d (pred n))
-(\lambda d:nat.sigma_p n (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
-  [ apply eq_sigma_p1
-    [ intros.
-      reflexivity
-    | intros.
-      apply sym_eq.
-      apply (trans_eq ? ? 
-       (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
-      [ apply false_to_eq_sigma_p
-        [ apply lt_to_le. 
-          assumption
-        | intros.
-          rewrite > lt_to_leb_false
-          [ reflexivity
-          | apply le_S_S.
-            assumption
-          ]
-        ]
-      | apply eq_sigma_p
-        [ intros.
-          rewrite > le_to_leb_true
-          [ reflexivity
-          | assumption
-          ]
-        | intros.
-          reflexivity
-        ]
+    | apply (divides_to_lt_O ? n)
+      [ assumption
+      | apply divides_gcd_m
       ]
-    ]
-  | rewrite < (sigma_p2' n n 
-               (\lambda d:nat.divides_b d (pred n))
-               (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O))
-               (\lambda x,y.(S O))).   
-    apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O)))
-    [ apply (eq_sigma_p_gh
-      (\lambda x:nat. (S O))
-      (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) )  )    
-      (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) )
-      (n*n)
-      (pred n)
-      (\lambda x:nat. 
-        divides_b (x/n) (pred n) 
-        \land (leb (S (x \mod n)) (x/n)
-        \land eqb (gcd (x \mod n) (x/n)) (S O)))
-      (\lambda x:nat.true)
-      )    
-      [ intros.
-        reflexivity
-      | intros.
-        cut ((i/n) \divides (pred n))
-        [ cut ((i \mod n ) \lt (i/n))
-          [ cut ((gcd (i \mod n) (i / n)) = (S O)) 
-            [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n)))
-              [ rewrite > Hcut3.
-                cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n))
-                [ rewrite > Hcut4.
-                  cut ((pred n)/ ((pred n)/(i/n)) = (i/n))
-                  [ rewrite > Hcut5.
-                    apply sym_eq.
-                    apply div_mod.
-                    apply (trans_lt O (S O) n)
-                    [ apply (lt_O_S O)
-                    | assumption
-                    ]
-                  | elim Hcut.
-                    rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?).
-                    rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?).
-                    rewrite > (div_times_ltO n2 (i/n))
-                    [ rewrite > H3.
-                      apply div_times_ltO.
-                      apply (divides_to_lt_O n2 (pred n))
-                      [ apply (n_gt_Uno_to_O_lt_pred_n n).
-                        assumption
-                      | apply (witness n2 (pred n) (i/n)).
-                        rewrite > sym_times.
-                        assumption
-                      ]
-                    | apply (divides_to_lt_O (i/n) (pred n))
-                      [ apply (n_gt_Uno_to_O_lt_pred_n n).
-                        assumption
-                      | apply (witness (i/n) (pred n) n2).
-                        assumption                                
-                      ]
-                    ]
-                  ]
-                | elim Hcut.
-                  cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n))))
-                  [ rewrite > Hcut4.
-                    rewrite > H3.
-                    rewrite < (sym_times n2 (i/n)).
-                    rewrite > (div_times_ltO n2 (i/n))
-                    [ rewrite > (div_times_ltO (i \mod n) n2)
-                      [ reflexivity                     
-                      | apply (divides_to_lt_O n2 (pred n))
-                        [ apply (n_gt_Uno_to_O_lt_pred_n n).
-                          assumption                      
-                        | apply (witness n2 (pred n) (i/n)).
-                          rewrite > sym_times.
-                          assumption
-                        ]
-                      ]
-                    | apply (divides_to_lt_O (i/n) (pred n))
-                      [ apply (n_gt_Uno_to_O_lt_pred_n n).
+    ]  
+    | cut (i \divides n)
+      [ cut (j \lt i)
+        [ cut ((gcd j i) = (S O) )
+          [ cut ((gcd (j*(n/i)) n) = n/i)
+            [ split
+              [ split
+                [ split
+                  [ reflexivity
+                  | rewrite > Hcut3.
+                    apply (cic:/matita/Z/dirichlet_product/div_div.con);
+                      assumption
+                  ]               
+                | rewrite > Hcut3.
+                  rewrite < divides_to_eq_times_div_div_times
+                  [ rewrite > div_n_n  
+                    [ apply sym_eq.
+                      apply times_n_SO.
+                    | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*)
                         assumption
-                      | assumption
-                      ]
                     ]
-                  | apply (sym_eq).
-                    apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
-                    [ apply (n_gt_Uno_to_O_lt_pred_n n).
+                  | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*)
                       assumption
-                    | assumption       
-                    ]
+                  | apply divides_n_n
                   ]
                 ]
-              | apply (sum_divisor_totient1_aux2);
-                assumption
+              | rewrite < (divides_to_times_div n i) in \vdash (? ? %)
+                [ rewrite > sym_times.
+                  apply (lt_times_r1)
+                  [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*)
+                      assumption
+                  | assumption
+                  ]
+                | apply (divides_to_lt_O i n); assumption
+                | assumption
+                ]               
               ]
-            | 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))
-              ).
-              apply (andb_true_true          
-               ((eqb (gcd (i\mod n) (i/n)) (S O)) 
-                \land 
-                (leb (S (i\mod n)) (i/n)))
-                     (divides_b (i/n) (pred n))
-              ).
-              rewrite > andb_sym.
-              rewrite > andb_sym in \vdash (? ? (? ? %) ?).
-              assumption
-            ]
-          | change with (S (i \mod n) \le (i/n)).
-            cut (leb (S (i \mod n)) (i/n) = true)
-            [ change with (
-                match (true) with
-                [ true  \Rightarrow (S (i \mod n)) \leq (i/n) 
-                | false \Rightarrow (S (i \mod n)) \nleq (i/n)]
-              ).
-              rewrite < Hcut1.  
-              apply (leb_to_Prop (S(i \mod n)) (i/n))
-            | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n))  ).
-              apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n)))
-                (eqb (gcd (i\mod n) (i/n)) (S O))
-              ).
-              rewrite > andb_sym in \vdash (? ? (? % ?) ?).
-              rewrite < (andb_assoc) in \vdash (? ? % ?).
-              assumption
-            ]
-          ]
-        | apply (divides_b_true_to_divides ).                   
-          apply (andb_true_true (divides_b (i/n) (pred n))
-                          (leb (S (i\mod n)) (i/n))).
-          apply (andb_true_true ( (divides_b (i/n) (pred n)) \land  (leb (S (i\mod n)) (i/n)) )
-            (eqb (gcd (i\mod n) (i/n)) (S O))
-          ).
-          rewrite < andb_assoc.
-          assumption.
-        ]
-      | intros.
-        apply (sum_divisor_totient1_aux_3);
-          assumption.        
-      | intros.
-        apply (sum_divisor_totient1_aux_4);
-          assumption.
-      | intros.
-        cut (j/(gcd (pred n) j) \lt n)
-        [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
-          [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j))
-            [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n))
-              [ apply (n_gt_Uno_to_O_lt_pred_n n).
-                assumption
-              | rewrite > sym_gcd.
-                apply lt_O_gcd.  
-                apply (n_gt_Uno_to_O_lt_pred_n n).
-                assumption
+            | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?)
+              [ rewrite > (sym_times j).
+                rewrite > times_n_SO in \vdash (? ? ? %).
+                rewrite < Hcut2.
+                apply eq_gcd_times_times_times_gcd.                
+              | apply (divides_to_lt_O i n); assumption
               | assumption
-              | apply divides_gcd_m
-              | rewrite > sym_gcd.
-                apply divides_gcd_m
               ]
-            | assumption
             ]
-          | assumption
+          | apply eqb_true_to_eq.
+            apply (andb_true_true_r (leb (S j) i)).            
+            assumption            
           ]
-        | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n)
-          [ apply (lt_to_divides_to_div_le)
-            [ rewrite > sym_gcd.
-              apply lt_O_gcd.
-              apply (n_gt_Uno_to_O_lt_pred_n n).
-              assumption
-            | apply divides_gcd_m
-            ]
-          | apply (lt_to_le_to_lt j (pred n) n)
-            [ assumption
-            | apply le_pred_n
-            ]
+        | change with ((S j) \le i).
+          cut((leb (S j) i) = true)
+          [ change with(
+            match (true) with
+            [ true  \Rightarrow ((S j) \leq i) 
+            | false \Rightarrow ((S j) \nleq i)]
+            ).
+            rewrite < Hcut1.
+            apply (leb_to_Prop)
+          | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).            
+            assumption
           ]
         ]
-      | intros.
-        apply (sum_divisor_totient1_aux_6);
-          assumption.
+        | apply (divides_b_true_to_divides).
+          assumption
       ]
-    | apply (sigma_p_true).
     ]
-  ]
-qed.
-
-
-(*there's a little difference between the following definition of the
-  theorem, and the abstract definition given before.
-  in fact (sigma_p n f p) works on (pred n), and not on n, as first element.
-  that's why in the definition of the theorem the summary is set equal to 
-  (pred n).
- *)
-theorem sum_divisor_totient: \forall n.
-sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n).
-intros.
-apply (nat_case1 n)
-[ intros.
-  simplify.
-  reflexivity
-| intros.
-  apply (nat_case1 m)
-  [ intros.
-    simplify.
-    reflexivity
-  | intros.
-    rewrite < H1.
-    rewrite < H.
-    rewrite > (pred_Sn m).
-    rewrite < H.
-    apply( sum_divisor_totient1).
-    rewrite > H.
-    rewrite > H1.
-    apply cic:/matita/algebra/finite_groups/lt_S_S.con.
-    apply lt_O_S
+  | apply (sigma_p_true).
   ]
 ]
-qed.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+qed.  
+    
+