From 6c8f66d57aa3da3b91ff6c76442424dfe2eeceaf Mon Sep 17 00:00:00 2001
From: Cristian Armentano <??>
Date: Sat, 30 Jun 2007 17:15:15 +0000
Subject: [PATCH] New definition of Euler's totient function. New theorems
 about sigma_p (invoked with an always true predicate). Theorem about the sum
 of totient invocations on the divisors of a natural number.

---
 matita/library/nat/euler_theorem.ma   | 185 ++++++-
 matita/library/nat/generic_sigma_p.ma |   2 +-
 matita/library/nat/iteration2.ma      | 352 ++++++++++++
 matita/library/nat/totient.ma         |  98 ++--
 matita/library/nat/totient1.ma        | 754 ++++++++++++++++++++++++++
 5 files changed, 1321 insertions(+), 70 deletions(-)
 create mode 100644 matita/library/nat/totient1.ma

diff --git a/matita/library/nat/euler_theorem.ma b/matita/library/nat/euler_theorem.ma
index d45c15dc3..ab7d8242e 100644
--- a/matita/library/nat/euler_theorem.ma
+++ b/matita/library/nat/euler_theorem.ma
@@ -17,24 +17,7 @@ set "baseuri" "cic:/matita/nat/euler_theorem".
 include "nat/map_iter_p.ma".
 include "nat/totient.ma".
 
-lemma gcd_n_n: \forall n.gcd n n = n.
-intro.elim n
-  [reflexivity
-  |apply le_to_le_to_eq
-    [apply divides_to_le
-      [apply lt_O_S
-      |apply divides_gcd_n
-      ]
-    |apply divides_to_le
-      [apply lt_O_gcd.apply lt_O_S
-      |apply divides_d_gcd
-        [apply divides_n_n|apply divides_n_n]
-      ]
-    ]
-  ]
-qed.
-
-
+(*
 lemma count_card: \forall p.\forall n.
 p O = false \to count (S n) p = card n p.
 intros.elim n
@@ -55,7 +38,7 @@ intros 3.apply (nat_case n)
 qed.
  
 
-(* a reformulation of totient using card insted of count *)
+( a reformulation of totient using card insted of count )
 
 lemma totient_card: \forall n. 
 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
@@ -70,15 +53,147 @@ intro.apply (nat_case n)
     ]
   ]
 qed.
+*)
 
+
+(*this obvious property is useful because simplify, sometimes,
+  "simplifies too much", and doesn't allow to obtain this simple result.
+ *)
+theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
+card (S n) p = (bool_to_nat (p (S n))) + (card n p).
+intros.
+simplify.
+reflexivity.
+qed.
+
+(* a reformulation of totient using card insted of sigma_p *)
+
+theorem totient_card_aux: \forall n,m: nat.
+m = n \to
+sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O)) 
+= card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
+intros.
+rewrite < H in \vdash (? ? (? % ? ?) ?).
+rewrite < H in \vdash (? ? ? (? % ?)).
+elim (m)
+[ rewrite > card_Sn.
+  cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
+  [ rewrite > Hcut.
+    simplify in \vdash (? ? ? %).
+    rewrite > true_to_sigma_p_Sn
+    [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
+      [ simplify in \vdash (? ? % ?).
+        reflexivity
+      | rewrite > gcd_O_n.
+        apply not_eq_to_eqb_false.
+        apply cic:/matita/nat/nat/not_eq_S.con.                
+        unfold Not.
+        intro.        
+        cut ( (S n) \le O)
+        [ apply (not_le_Sn_n n ?).
+          apply (transitive_le (S n) O n ? ?);
+          [ apply (Hcut1)
+          | apply (le_O_n n)
+          ]
+        | rewrite > H1.
+          apply le_n
+        ]
+      ]
+    | assumption
+    ]
+  | apply eq_to_eqb_true.
+    rewrite > gcd_SO_n.
+    reflexivity   
+  ]
+| cut ((eqb (gcd (S (S n1)) (S (S n))) (S O))  = true 
+    \lor (eqb (gcd (S (S n1)) (S (S n))) (S O))  = false)
+  [ elim Hcut
+    [ rewrite > card_Sn.
+      rewrite > true_to_sigma_p_Sn
+      [ rewrite > H2.
+        simplify in \vdash (? ? ? (? % ?)).
+        apply eq_f.
+        assumption
+      | assumption
+      ]      
+    | rewrite > card_Sn.
+      rewrite > false_to_sigma_p_Sn
+      [ rewrite > H2.
+        simplify in \vdash (? ? ? (? % ?)).
+        rewrite > sym_plus.
+        rewrite < plus_n_O.
+        assumption
+      | assumption  
+      ]
+    ]
+  | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
+    [ left.
+      reflexivity
+    | right.
+      reflexivity
+    ]
+  ]
+]
+qed.
+  
+
+lemma totient_card: \forall n.
+totient n = card n (\lambda i.eqb (gcd i n) (S O)).
+intros.
+elim n
+[ simplify.
+  reflexivity
+| elim n1
+  [ simplify.
+    reflexivity
+  |
+    (*unfold card.
+    intros.*)
+    (* here simplify creates problems: it seems it simplifies too much. I had to 
+     * introduce the obvious theorem card_Sn.
+     *)
+    rewrite > card_Sn.
+    rewrite > (gcd_n_n (S (S n2))).
+    cut ((eqb (S (S n2)) (S O)) = false)
+    [ rewrite > Hcut.
+      simplify in \vdash (? ? ? (? % ?)).
+      rewrite > sym_plus.
+      rewrite < (plus_n_O).
+      unfold totient.      
+      apply (totient_card_aux n2 n2).
+      reflexivity    
+    | apply not_eq_to_eqb_false.
+      apply cic:/matita/nat/nat/not_eq_S.con.
+      unfold Not.
+      intro.
+      cut ( (S n2) \le O)
+        [ apply (not_le_Sn_n n2 ?).
+          apply (transitive_le (S n2) O n2 ? ?);
+          [ apply (Hcut)
+          | apply (le_O_n n2)
+          ]
+        | rewrite > H2.
+          apply le_n
+        ]
+    ]
+  ]
+]
+qed.
+  
 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
 intros 3.elim H
   [rewrite > pi_p_S.
    cut (eqb (gcd (S O) n) (S O) = true)
     [rewrite > Hcut.
-     change with ((gcd n (S O)) = (S O)).autobatch
-    |apply eq_to_eqb_true.autobatch
+     change with ((gcd n (S O)) = (S O)).
+     apply (transitive_eq nat (gcd n (S O)) (gcd (S O) n) (S O) ? ?);
+     [ apply (sym_eq nat (gcd (S O) n) (gcd n (S O)) ?).
+       apply (symmetric_gcd (S O) n).
+     | apply (gcd_SO_n n).
+     ]
+    |apply eq_to_eqb_true.
+     apply (gcd_SO_n n)
     ]
   |rewrite > pi_p_S.
    apply eqb_elim
@@ -189,11 +304,18 @@ split
             |apply mod_O_to_divides
               [assumption
               |rewrite > distr_times_minus.
-               autobatch
+               apply (divides_to_mod_O n (minus (times a j) (times a i)) ? ?);
+               [ apply (H3).
+               | apply (eq_mod_to_divides (times a j) (times a i) n ? ?);
+                [ apply (H3).
+                |apply (sym_eq nat (mod (times a i) n) (mod (times a j) n) ?).
+                 apply (H13).
+                ]
+               ]
               ]
             ]
           ]
-        |autobatch
+        | apply (le_minus_m j i).
         ]
       ]
     |intro.assumption
@@ -214,11 +336,17 @@ split
             |apply mod_O_to_divides
               [assumption
               |rewrite > distr_times_minus.
-               autobatch
+               apply (divides_to_mod_O n (minus (times a i) (times a j)) ? ?);
+               [apply (H3).
+               | apply (eq_mod_to_divides (times a i) (times a j) n ? ?);
+                 [apply (H3).
+                 |apply (H13).
+                 ]
+               ]
               ]
             ]
           ]
-        |autobatch
+        | apply (le_minus_m i j).
         ]
       ]
     ]
@@ -229,7 +357,7 @@ theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n. 
 intros.
 cut (O < a)
-  [apply divides_to_congruent
+  [ apply divides_to_congruent
     [apply (trans_lt ? (S O)).apply lt_O_S. assumption
     |change with (O < exp a (totient n)).apply lt_O_exp.assumption
     |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
@@ -281,6 +409,5 @@ cut (O < a)
           [assumption|apply sym_eq.assumption] 
         ]
       ]     
-    ]       
-qed.  
-     
\ No newline at end of file
+    ]
+qed.
diff --git a/matita/library/nat/generic_sigma_p.ma b/matita/library/nat/generic_sigma_p.ma
index ed9f59b0a..8ab37e999 100644
--- a/matita/library/nat/generic_sigma_p.ma
+++ b/matita/library/nat/generic_sigma_p.ma
@@ -982,7 +982,7 @@ theorem distributive_times_plus_sigma_p_generic: \forall A:Type.
   \to
 
 ((timesA k (sigma_p_gen n p A g basePlusA plusA)) = 
- (sigma_p_gen n p A (\lambda i:nat.(timesA (g i) k)) basePlusA plusA)).
+ (sigma_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
 intros.
 elim n
 [ simplify.
diff --git a/matita/library/nat/iteration2.ma b/matita/library/nat/iteration2.ma
index 53cc949a2..4f0238498 100644
--- a/matita/library/nat/iteration2.ma
+++ b/matita/library/nat/iteration2.ma
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/iteration2".
 include "nat/primes.ma".
 include "nat/ord.ma".
 include "nat/generic_sigma_p.ma".
+include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
 
 
 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
@@ -229,3 +230,354 @@ apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g)
 ]
 qed.
 
+(*some properties of sigma_p invoked with an "always true" predicate (in this 
+  way sigma_p just counts the elements, without doing any control) or with
+  the nat \to nat function which always returns (S O).
+  It 's not easily possible proving these theorems in a general form 
+  in generic_sigma_p.ma
+ *)
+
+theorem sigma_p_true: \forall n:nat.
+(sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
+intros.
+elim n
+[ simplify.
+  reflexivity
+| rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
+  [ rewrite > H.
+    simplify.
+    reflexivity
+  | reflexivity 
+  ]
+]
+qed.
+
+theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
+sigma_p n g (\lambda n:nat. (S O)) = 
+sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
+intros.
+elim n
+[ simplify.
+  reflexivity
+| cut ((g n1) = true \lor (g n1) = false)
+  [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
+    [ elim Hcut
+      [ rewrite > H1.
+        rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
+        [ simplify.
+          apply eq_f.
+          assumption
+        | assumption
+        ]
+      | rewrite > H1.
+        rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
+        [ simplify.
+          assumption
+        | assumption
+        ]
+      ]
+    | reflexivity
+    ]
+  | elim (g n1)
+    [ left.
+      reflexivity
+    | right.
+      reflexivity
+    ]
+  ]
+]
+qed.
+
+(* I introduce an equivalence in the form map_iter_i in order to use
+ * the existing result about permutation in that part of the library.
+ *) 
+ 
+theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat. 
+map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
+intros.
+elim n
+[ simplify.
+  rewrite < plus_n_O.
+  reflexivity
+| rewrite > true_to_sigma_p_Sn
+  [ simplify in \vdash (? ? % ?).
+    rewrite < plus_n_O.
+    apply eq_f.
+    assumption
+  | reflexivity
+  ]
+]
+qed.
+
+theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
+sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) = 
+sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
+intros.
+elim n
+[ simplify.
+  reflexivity
+| rewrite > true_to_sigma_p_Sn
+  [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
+    [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
+      [ rewrite > assoc_plus in \vdash (? ? ? %).
+        rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
+        rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
+        rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
+        rewrite < assoc_plus in \vdash (? ? ? %).
+        apply eq_f.
+        assumption
+      | reflexivity
+      ]
+    | reflexivity
+    ]
+  | reflexivity
+  ]
+]
+qed.
+
+
+theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
+sigma_p (n*m) (\lambda x:nat.true) f =
+sigma_p m (\lambda x:nat.true) 
+    (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
+intro.
+elim n
+[ simplify.
+  elim m
+  [ simplify.
+    reflexivity
+  | rewrite > true_to_sigma_p_Sn
+    [ rewrite < H.
+      reflexivity
+    | reflexivity
+    ]
+  ]
+| change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) + 
+  (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
+  rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
+  rewrite > (sym_times (S n1) m).
+  rewrite < (times_n_Sm m  n1).
+  rewrite > sigma_p_plus in \vdash (? ? % ?).
+  apply eq_f2
+  [ rewrite < (sym_times m n1).
+    apply eq_sigma_p
+    [ intros. 
+      reflexivity
+    | intros.
+      rewrite < (sym_plus ? (m * n1)).
+      reflexivity
+    ]
+  | rewrite > (sym_times m n1).
+    apply H
+  ]
+]
+qed.
+
+theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
+sigma_p (n *m) (\lambda c:nat.true) f =
+sigma_p  n (\lambda c:nat.true) 
+  (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
+intros.
+rewrite > sym_times.
+apply eq_sigma_p_sigma_p_times1.
+qed.
+
+
+theorem sigma_p_times:\forall n,m:nat. 
+\forall f,f1,f2:nat \to bool.
+\forall g:nat \to nat \to nat. 
+\forall g1,g2: nat \to nat.
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
+(sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) = 
+sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)). 
+intros.
+
+rewrite > (sigma_P_SO_to_sigma_p_true ).
+rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
+[ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
+  rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? 
+           (\lambda i.g (div i (S n)) (mod i (S n))))
+  [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
+    rewrite < S_pred
+    [ rewrite > eq_sigma_p_sigma_p_times2.
+      apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true) 
+        (\lambda a. sigma_p (S m) (\lambda c:nat.true) 
+                (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
+      [ apply eq_sigma_p;intros
+        [ reflexivity
+        | apply eq_sigma_p;intros
+          [ reflexivity
+          | 
+            rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n)) 
+                                                  ((x1*(S n) + x) \mod (S n)) x1 x)
+            [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n)) 
+                                                  ((x1*(S n) + x) \mod (S n)) x1 x)
+              [ rewrite > H3
+                [ apply bool_to_nat_andb
+                | assumption
+                | assumption
+                ]
+              | apply div_mod_spec_div_mod.
+                apply lt_O_S
+              | constructor 1
+                [ assumption
+                | reflexivity
+                ]
+              ]
+            | apply div_mod_spec_div_mod.
+              apply lt_O_S
+            | constructor 1
+              [ assumption
+              | reflexivity
+              ]
+            ]
+          ]
+        ]
+      | apply (trans_eq ? ? 
+         (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
+         (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
+        [ apply eq_sigma_p;intros
+          [ reflexivity
+          | rewrite > distributive_times_plus_sigma_p.
+            apply eq_sigma_p;intros
+            [ reflexivity
+            | rewrite > sym_times. 
+              reflexivity
+            ]
+          ]
+        | apply sym_eq.
+          rewrite > sigma_P_SO_to_sigma_p_true.
+          rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
+          rewrite > sym_times. 
+          rewrite > distributive_times_plus_sigma_p.
+          apply eq_sigma_p;intros
+          [ reflexivity
+          | rewrite > distributive_times_plus_sigma_p.
+            rewrite < sym_times.
+            rewrite > distributive_times_plus_sigma_p.
+            apply eq_sigma_p;
+              intros; reflexivity            
+          ]
+        ]
+      ]
+    | apply lt_O_times_S_S
+    ]
+    
+  | unfold permut.
+    split
+    [ intros.
+      rewrite < plus_n_O.
+      apply le_S_S_to_le.
+      rewrite < S_pred in \vdash (? ? %)
+      [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
+        apply H
+        [ apply lt_mod_m_m.
+          unfold lt. 
+          apply le_S_S.
+          apply le_O_n 
+        | apply (lt_times_to_lt_l n).
+          apply (le_to_lt_to_lt ? i)
+          [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
+            [ rewrite > sym_plus.
+              apply le_plus_n
+            | unfold lt. 
+              apply le_S_S.
+              apply le_O_n
+            ]
+          | unfold lt.
+            rewrite > S_pred in \vdash (? ? %)
+            [ apply le_S_S.
+              rewrite > plus_n_O in \vdash (? ? %).
+              rewrite > sym_times. 
+              assumption
+            | apply lt_O_times_S_S
+            ]
+          ]
+        ]
+      | apply lt_O_times_S_S
+      ]
+    | rewrite < plus_n_O.
+      unfold injn.
+      intros.
+      cut (i < (S n)*(S m))
+      [ cut (j < (S n)*(S m))
+        [ cut ((i \mod (S n)) < (S n))
+          [ cut ((i/(S n)) < (S m))
+            [ cut ((j \mod (S n)) < (S n))
+              [ cut ((j/(S n)) < (S m))
+                [ rewrite > (div_mod i (S n))
+                  [ rewrite > (div_mod j (S n))
+                    [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
+                      rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
+                      rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
+                      rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
+                      rewrite > H6.
+                      reflexivity
+                    | unfold lt.
+                      apply le_S_S.
+                      apply le_O_n
+                    ]
+                  | unfold lt. 
+                    apply le_S_S.
+                    apply le_O_n
+                  ]
+                | apply (lt_times_to_lt_l n).
+                  apply (le_to_lt_to_lt ? j)
+                  [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
+                    [ rewrite > sym_plus.
+                      apply le_plus_n
+                    | unfold lt. apply le_S_S.
+                      apply le_O_n
+                    ]
+                  | rewrite < sym_times. 
+                    assumption                    
+                  ]
+                ]
+              | apply lt_mod_m_m.
+                unfold lt. 
+                apply le_S_S.
+                apply le_O_n
+              ]
+            | apply (lt_times_to_lt_l n).
+              apply (le_to_lt_to_lt ? i)
+              [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
+                [ rewrite > sym_plus.
+                  apply le_plus_n
+                | unfold lt. 
+                  apply le_S_S.
+                  apply le_O_n
+                ]
+              | rewrite < sym_times. 
+                assumption
+              ]
+            ]
+          | apply lt_mod_m_m.
+            unfold lt. 
+            apply le_S_S.
+            apply le_O_n
+          ]
+        | unfold lt.
+          rewrite > S_pred in \vdash (? ? %)
+          [ apply le_S_S.
+            assumption
+          | apply lt_O_times_S_S 
+          ]
+        ]
+      | unfold lt.
+        rewrite > S_pred in \vdash (? ? %)
+        [ apply le_S_S.
+          assumption
+        | apply lt_O_times_S_S 
+        ]
+      ]
+    ]
+  | intros.
+    apply False_ind.
+    apply (not_le_Sn_O m1 H4)
+  ]
+| apply lt_O_times_S_S
+]
+qed.
diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index b4f575a40..730ec8b56 100644
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -14,62 +14,80 @@
 
 set "baseuri" "cic:/matita/nat/totient".
 
-include "nat/count.ma".
 include "nat/chinese_reminder.ma".
+include "nat/iteration2.ma".
 
+(*a new definition of totient, which uses sigma_p instead of sigma *)
+(*there's a little difference between this definition and the classic one:
+  the classic definition of totient is:
+   
+    phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
+   (so this definition considers the values i=1,2,...,n)
+  
+  sigma_p doesn't work ok the value n (but the first value it works on is (pred n))
+  but works also on 0. That's not a problem, in fact
+   - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. 
+   - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. 
+   
+ *)
 definition totient : nat \to nat \def
-\lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
-
-theorem totient3: totient (S(S(S O))) = (S(S O)).
-reflexivity.
-qed.
-
-theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
-reflexivity.
-qed.
+\lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
 
+                                        
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
-intro.
-apply (nat_case n)
-  [intros.simplify.reflexivity
-  |intros 2.apply (nat_case m1)
-    [rewrite < sym_times.
-     rewrite < (sym_times (totient O)).
-     simplify.intro.reflexivity.
-     |intros.
-      unfold totient.
-      apply (count_times m m2 ? ? ? 
-             (\lambda b,a. cr_pair (S m) (S m2) a b) 
-             (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)))
-       [intros.unfold cr_pair.
-        apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
+intros.
+unfold totient.
+apply (nat_case1 n)
+[ apply (nat_case1 m)
+  [ intros.
+    simplify.
+    reflexivity
+  | intros.
+    simplify.
+    reflexivity
+  ]
+| apply (nat_case1 m)
+  [ intros.
+    change in \vdash (? ? ? (? ? %)) with (O).
+    rewrite > (sym_times (S m1) O).
+    rewrite > sym_times in \vdash (? ? ? %).
+    simplify.
+    reflexivity  
+  | intros.
+    rewrite > H2 in H.
+    rewrite > H1 in H.    
+    apply (sigma_p_times m2 m1 ? ? ? 
+            (\lambda b,a. cr_pair (S m2) (S m1) a b) 
+            (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
+   [intros.unfold cr_pair.
+        apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
           [unfold min.
            apply le_min_aux_r
           |unfold lt.
-           apply (nat_case ((S m)*(S m2)))
+           apply (nat_case ((S m2)*(S m1)))
             [apply le_n|intro.apply le_n]
           ]
        |intros.
-        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-        intro.elim H3.
-        apply H4
+        generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+        intro.elim H5.
+        apply H6
        |intros.
-        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-        intro.elim H3.
-        apply H5
+        generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+        intro.elim H5.
+        apply H7
        |intros.
-        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-        intro.elim H3.
+        generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+        intro.elim H5.
         apply eqb_elim
           [intro.
            rewrite > eq_to_eqb_true
              [rewrite > eq_to_eqb_true
                [reflexivity
-               |rewrite < H4.
+               |rewrite < H6.
                 rewrite > sym_gcd.
                 rewrite > gcd_mod
-                  [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
+                  [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
                     [unfold lt.apply le_S_S.apply le_O_n
                     |unfold lt.apply le_S_S.apply le_O_n
                     |assumption
@@ -77,10 +95,10 @@ apply (nat_case n)
                   |unfold lt.apply le_S_S.apply le_O_n
                   ]
                ]           
-            |rewrite < H5.
+            |rewrite < H7.
              rewrite > sym_gcd.
              rewrite > gcd_mod
-               [apply (gcd_times_SO_to_gcd_SO ? ? (S m))
+               [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
                   [unfold lt.apply le_S_S.apply le_O_n
                   |unfold lt.apply le_S_S.apply le_O_n
                   |rewrite > sym_times.assumption
@@ -92,17 +110,17 @@ apply (nat_case n)
            apply eqb_elim
            [intro.apply eqb_elim
               [intro.apply False_ind.
-               apply H6.
+               apply H8.
                apply eq_gcd_times_SO
                  [unfold lt.apply le_S_S.apply le_O_n.
                  |unfold lt.apply le_S_S.apply le_O_n.
                  |rewrite < gcd_mod
-                    [rewrite > H4.
+                    [rewrite > H6.
                      rewrite > sym_gcd.assumption
                     |unfold lt.apply le_S_S.apply le_O_n
                     ]
                  |rewrite < gcd_mod
-                    [rewrite > H5.
+                    [rewrite > H7.
                      rewrite > sym_gcd.assumption
                     |unfold lt.apply le_S_S.apply le_O_n
                     ]
diff --git a/matita/library/nat/totient1.ma b/matita/library/nat/totient1.ma
new file mode 100644
index 000000000..feaf1314b
--- /dev/null
+++ b/matita/library/nat/totient1.ma
@@ -0,0 +1,754 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/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
+ * function:
+ 
+   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).
+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.
+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).             
+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
+]
+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.
+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 (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)
+            ]
+          ]
+        | 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);
+          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
+      ]
+    ]
+  ]
+| 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))
+                [ assumption
+                | assumption
+                | apply (divides_gcd_n (pred 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))
+                [ assumption
+                | assumption
+                | apply divides_gcd_n
+                ]
+              | 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) ? ?)
+              [ assumption
+              | simplify.
+                rewrite > NdivM_times_M_to_N
+                [ assumption
+                | assumption
+                | apply divides_gcd_n
+                ]
+              ]
+            | 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))
+                | assumption
+                ]                
+              ]
+            | 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);
+            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
+          ]
+        | assumption
+        ]
+      ]
+    | apply (witness n c b).
+      rewrite > (sym_times n b).
+      assumption
+    ]
+  | 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)
+  ]
+]
+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
+          ]
+        | 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_totiet)
+ *)        
+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
+        ]
+      ]
+    ]
+  | 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).
+                        assumption
+                      | assumption
+                      ]
+                    ]
+                  | apply (sym_eq).
+                    apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n))
+                    [ apply (n_gt_Uno_to_O_lt_pred_n n).
+                      assumption
+                    | assumption       
+                    ]
+                  ]
+                ]
+              | apply (sum_divisor_totient1_aux2);
+                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
+              | assumption
+              | apply divides_gcd_m
+              | rewrite > sym_gcd.
+                apply divides_gcd_m
+              ]
+            | assumption
+            ]
+          | 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
+            ]
+          ]
+        ]
+      | intros.
+        apply (sum_divisor_totient1_aux_6);
+          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
+  ]
+]
+qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-- 
2.39.2