From: Cristian Armentano <??>
Date: Wed, 27 Jun 2007 18:05:37 +0000 (+0000)
Subject: new gcd properties, and theorems for totient, and theorems for totient1
X-Git-Tag: 0.4.95@7852~388
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77440acc493b0e04b7e009b942c6a3268a46c141;p=helm.git

new gcd properties, and theorems for totient, and theorems for totient1

--this line, and those below, will be ignored--

M    minus.ma
M    le_arith.ma
M    lt_arith.ma
M    div_and_mod.ma
M    div_and_mod_new.ma
M    orders.ma
A    propr_div_mod_lt_le_totient1_aux.ma
A    gcd_properties1.ma
---

diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma
index 537d3bcf0..d7750e39a 100644
--- a/matita/library/nat/div_and_mod.ma
+++ b/matita/library/nat/div_and_mod.ma
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/div_and_mod".
 include "datatypes/constructors.ma".
 include "nat/minus.ma".
 
+
 let rec mod_aux p m n: nat \def
 match (leb m n) with
 [ true \Rightarrow m
@@ -331,3 +332,14 @@ 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.
+
diff --git a/matita/library/nat/div_and_mod_new.ma b/matita/library/nat/div_and_mod_new.ma
index 2f881b155..f08a5f94e 100644
--- a/matita/library/nat/div_and_mod_new.ma
+++ b/matita/library/nat/div_and_mod_new.ma
@@ -358,3 +358,12 @@ 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.
diff --git a/matita/library/nat/gcd_properties1.ma b/matita/library/nat/gcd_properties1.ma
new file mode 100644
index 000000000..aa9783a96
--- /dev/null
+++ b/matita/library/nat/gcd_properties1.ma
@@ -0,0 +1,589 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/gcd_properties1".
+
+include "nat/propr_div_mod_lt_le_totient1_aux.ma".
+
+(* this file contains some important properites of gcd in N *)
+
+(*it's a generalization of the existing theorem divides_gcd_aux (in which
+  c = 1), proved in file gcd.ma
+ *)
+theorem divides_times_gcd_aux: \forall p,m,n,d,c. 
+O \lt c \to O < n \to n \le m \to n \le p \to
+d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n. 
+intro.
+elim p
+[ absurd (O < n)
+  [ assumption
+  | apply le_to_not_lt.
+    assumption
+  ]
+| simplify.
+  cut (n1 \divides m \lor n1 \ndivides m)
+  [ elim Hcut
+    [ rewrite > divides_to_divides_b_true
+      [ simplify.
+        assumption
+      | assumption
+      | assumption
+      ]
+    | rewrite > not_divides_to_divides_b_false
+      [ simplify.
+        apply H
+        [ assumption
+        | cut (O \lt m \mod n1 \lor O = m \mod n1)
+          [ elim Hcut1
+            [ assumption
+            | absurd (n1 \divides m)
+              [ apply mod_O_to_divides
+                [ assumption
+                | apply sym_eq.
+                  assumption
+                ]
+              | assumption
+              ]
+            ]
+          | apply le_to_or_lt_eq.
+            apply le_O_n
+          ]
+        | apply lt_to_le.
+          apply lt_mod_m_m.
+          assumption
+        | apply le_S_S_to_le.
+          apply (trans_le ? n1)
+          [ change with (m \mod n1 < n1).
+            apply lt_mod_m_m.
+            assumption
+          | assumption
+          ]
+        | assumption
+        | rewrite < times_mod
+          [ rewrite < (sym_times c m).
+            rewrite < (sym_times c n1).
+            apply divides_mod
+            [ rewrite > (S_pred c)
+              [ rewrite > (S_pred n1)
+                [ apply (lt_O_times_S_S)
+                | assumption
+                ]
+              | assumption
+              ]
+            | assumption
+            | assumption
+            ]
+          | assumption
+          | assumption
+          ]
+        ]
+      | assumption
+      | assumption
+      ]
+    ]
+  | apply (decidable_divides n1 m).
+    assumption
+  ]
+]
+qed.
+
+(*it's a generalization of the existing theorem divides_gcd_d (in which
+  c = 1), proved in file gcd.ma
+ *)
+theorem divides_d_times_gcd: \forall m,n,d,c. 
+O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m. 
+intros.
+change with
+(d \divides c *
+match leb n m with
+  [ true \Rightarrow 
+    match n with 
+    [ O \Rightarrow m
+    | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+  | false \Rightarrow 
+    match m with 
+    [ O \Rightarrow n
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+apply (leb_elim n m)
+[ apply (nat_case1 n)
+  [ simplify.
+    intros.
+    assumption
+  | intros.
+    change with (d \divides c*gcd_aux (S m1) m (S m1)).
+    apply divides_times_gcd_aux
+    [ assumption
+    | unfold lt.
+      apply le_S_S.
+      apply le_O_n
+    | assumption
+    | apply (le_n (S m1))
+    | assumption
+    | rewrite < H3.
+      assumption
+    ]
+  ]
+| apply (nat_case1 m)
+  [ simplify.
+    intros.
+    assumption
+  | intros.
+    change with (d \divides c * gcd_aux (S m1) n (S m1)).
+    apply divides_times_gcd_aux
+    [ unfold lt.
+      change with (O \lt c).
+      assumption
+    | apply lt_O_S
+    | apply lt_to_le.
+      apply not_le_to_lt.
+      assumption
+    | apply (le_n (S m1)).
+    | assumption
+    | rewrite < H3.
+      assumption
+    ]
+  ]
+]
+qed.
+
+(* 2 basic properties of divides predicate *)
+theorem aDIVb_to_bDIVa_to_aEQb:
+\forall a,b:nat.
+a \divides b \to b \divides a \to a = b.
+intros.
+apply antisymmetric_divides;
+  assumption.
+qed.
+
+
+theorem O_div_c_to_c_eq_O: \forall c:nat.
+O \divides c \to c = O.
+intros.
+apply aDIVb_to_bDIVa_to_aEQb
+[ apply divides_n_O
+| assumption
+]
+qed.
+
+(* an alternative characterization for gcd *)
+theorem gcd1: \forall a,b,c:nat.
+c \divides a \to c \divides b \to
+(\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
+intros.
+elim (H2 ((gcd a b)))
+[ apply (aDIVb_to_bDIVa_to_aEQb (gcd a b) c)
+  [ apply (witness (gcd a b) c n2).
+    assumption
+  | apply divides_d_gcd;
+      assumption
+  ]
+| apply divides_gcd_n
+| rewrite > sym_gcd.
+  apply divides_gcd_n
+]
+qed.
+
+
+theorem eq_gcd_times_times_eqv_times_gcd: \forall a,b,c:nat.
+(gcd (c*a) (c*b)) = c*(gcd a b).
+intros.
+apply (nat_case1 c)
+[ intros. 
+  simplify.
+  reflexivity
+| intros.
+  rewrite < H. 
+  apply (nat_case1 a)
+  [ intros.
+    rewrite > (sym_times c O).
+    simplify.
+    reflexivity
+  | intros.
+    rewrite < H1.
+    apply (nat_case1 b)
+    [ intros.
+      rewrite > (sym_times ? O).
+      rewrite > (sym_gcd a O).
+      rewrite > sym_gcd.
+      simplify.
+      reflexivity
+    | intros.
+      rewrite < H2.
+      apply gcd1
+      [ apply divides_times
+        [ apply divides_n_n
+        | apply divides_gcd_n.
+        ]
+      | apply divides_times
+        [ apply divides_n_n
+        | rewrite > sym_gcd.  
+          apply divides_gcd_n
+        ]
+      | intros.
+        apply (divides_d_times_gcd)
+        [ rewrite > H.
+          apply lt_O_S  
+        | assumption
+        | assumption
+        ]
+      ]
+    ]
+  ]
+]
+qed.
+
+
+theorem associative_nat_gcd: associative nat gcd.
+change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
+intros.
+apply gcd1
+[ apply divides_d_gcd
+  [ apply (trans_divides ? (gcd b c) ?)
+    [ apply divides_gcd_m
+    | apply divides_gcd_n
+    ]
+  | apply divides_gcd_n
+  ]
+| apply (trans_divides ? (gcd b c) ?)
+  [ apply divides_gcd_m
+  | apply divides_gcd_m
+  ]
+| intros.
+  cut (d \divides a \land d \divides b)
+  [ elim Hcut.
+    cut (d \divides (gcd b c))
+    [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
+    | apply (divides_d_gcd c b d H1 H3)
+    ]
+  | split
+    [ apply (trans_divides d (gcd a b) a H).
+      apply divides_gcd_n
+    | apply (trans_divides d (gcd a b) b H).
+      apply divides_gcd_m
+    ]
+  ]
+]
+qed.
+
+theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat.
+a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
+intros.
+apply (nat_case1 a)
+[ intros.
+  apply (nat_case1 b)
+  [ intros.
+    cut (d = 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 (O_div_c_to_c_eq_O (b*c) H)
+        ]
+      ]
+    | rewrite < H1.
+      apply lt_O_gcd.
+      rewrite > H3.
+      apply lt_O_S
+    ]
+  ]
+| intros.
+  rewrite < H2.
+  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_eqv_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
+          | assumption
+          ]
+        | assumption
+        | assumption    
+        ]
+      | 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
+    ]
+  ]
+]
+qed.
+
+theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat. 
+(gcd (a+m*b) b) = d \to (gcd a b) = d.
+intros.
+apply gcd1
+[ rewrite > (minus_plus_m_m a (m*b)).
+  apply divides_minus
+  [ rewrite < H.
+    apply divides_gcd_n
+  | rewrite > (times_n_SO d).
+    rewrite > (sym_times d ?).
+    apply divides_times
+    [ apply divides_SO_n
+    | rewrite < H.
+      apply divides_gcd_m
+    ]
+  ]
+| rewrite < H.
+  apply divides_gcd_m
+| intros.
+  rewrite < H.
+  apply divides_d_gcd
+  [ assumption
+  | apply divides_plus
+    [ assumption
+    | rewrite > (times_n_SO d1).
+      rewrite > (sym_times d1 ?).
+      apply divides_times
+      [ apply divides_SO_n
+      | assumption
+      ]
+    ]
+  ]
+]
+qed.
+
+theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat. 
+(gcd (a+m*b) b) = (gcd a b).
+intros.
+apply sym_eq.
+apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m).
+reflexivity.
+qed.
+
+theorem gcd_div_div_eq_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_eqv_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 gcdSO_divides_divides_times_divides: \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.
+  elim H1.
+  elim H2.
+  rewrite > H5.
+  rewrite > (sym_times e f).
+  apply (divides_times)
+  [ 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)
+    | 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). 
+ *)
+theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat.
+(gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
+intros.
+apply gcd1
+[ apply divides_times; 
+    apply divides_gcd_n
+| apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c))
+  [ apply gcd1
+    [ apply divides_SO_n  
+    | apply divides_SO_n
+    | intros.
+      cut (d \divides a)
+      [ cut (d \divides b)
+        [ rewrite < H.
+          apply (divides_d_gcd b a d Hcut1 Hcut)
+        | apply (trans_divides d (gcd b c) b)
+          [ assumption
+          | apply (divides_gcd_n)
+          ]
+        ]
+      | apply (trans_divides d (gcd a c) a)
+        [ assumption
+        | apply (divides_gcd_n)
+        ]
+      ]
+    ]
+  | apply (divides_gcd_m)
+  | apply (divides_gcd_m)      
+  ]
+| intros.
+  rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)).
+  rewrite > (sym_times (gcd a c) b).
+  rewrite > (sym_times (gcd a c) c).
+  rewrite < (eq_gcd_times_times_eqv_times_gcd a c b).
+  rewrite < (eq_gcd_times_times_eqv_times_gcd a c c).
+  apply (divides_d_gcd)
+  [ apply (divides_d_gcd)
+    [ rewrite > (times_n_SO d).
+      apply (divides_times)
+      [ assumption
+      | apply divides_SO_n
+      ]
+    | rewrite > (times_n_SO d).
+      apply (divides_times)
+      [ assumption
+      | apply divides_SO_n
+      ]
+    ]
+  | apply (divides_d_gcd)
+    [ rewrite > (times_n_SO d).
+      rewrite > (sym_times d (S O)).
+      apply (divides_times)
+      [ apply (divides_SO_n)
+      | assumption
+      ]
+    | rewrite < (sym_times a b).
+      assumption
+    ]
+  ]
+]
+qed.
+  
+  
+theorem gcd_eq_gcd_minus: \forall a,b:nat.
+a \lt b \to (gcd a b) = (gcd (b - a) b).
+intros.
+apply sym_eq.
+apply gcd1
+[ apply (divides_minus (gcd a b) b a)
+  [ apply divides_gcd_m
+  | apply divides_gcd_n
+  ]
+| apply divides_gcd_m
+| intros.
+  elim H1.
+  elim H2.
+  cut(b = (d*n2) + a) 
+  [ cut (b - (d*n2) = a)
+    [ rewrite > H4 in Hcut1.
+      rewrite < (distr_times_minus d n n2) in Hcut1.
+      apply divides_d_gcd
+      [ assumption
+      | apply (witness d a (n - n2)).
+        apply sym_eq.
+        assumption
+      ]
+    | apply (plus_to_minus ? ? ? Hcut)      
+    ]
+  | rewrite > sym_plus.
+    apply (minus_to_plus)
+    [ apply lt_to_le.
+      assumption
+    | assumption
+    ]
+  ]
+]
+qed.
+
diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma
index 90f3e182b..9ab53fd74 100644
--- a/matita/library/nat/le_arith.ma
+++ b/matita/library/nat/le_arith.ma
@@ -131,4 +131,15 @@ apply nat_elim2;intros
      assumption
     ]
   ]
-qed.
\ No newline at end of file
+qed.
+
+(*0 and times *)
+theorem O_lt_const_to_le_times_const:  \forall a,c:nat.
+O \lt c \to a \le a*c.
+intros.
+rewrite > (times_n_SO a) in \vdash (? % ?).
+apply le_times
+[ apply le_n
+| assumption
+]
+qed.
diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma
index f0fdbdbd6..e71514726 100644
--- a/matita/library/nat/lt_arith.ma
+++ b/matita/library/nat/lt_arith.ma
@@ -63,11 +63,61 @@ rewrite > sym_plus.
 rewrite > (sym_plus q).assumption.
 qed.
 
+theorem le_to_lt_to_plus_lt: \forall a,b,c,d:nat.
+a \le c \to b \lt d \to (a + b) \lt (c+d).
+intros.
+cut (a \lt c \lor a = c)
+[ elim Hcut
+  [ apply (lt_plus );
+      assumption
+  | rewrite > H2.
+    apply (lt_plus_r c b d).
+    assumption
+  ]
+| apply le_to_or_lt_eq.
+  assumption
+]
+qed.
+
+
 (* times and zero *)
 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
+theorem lt_times_eq_O: \forall a,b:nat.
+O \lt a \to (a * b) = O \to b = O.
+intros.
+apply (nat_case1 b)
+[ intros.
+  reflexivity
+| intros.
+  rewrite > H2 in H1.
+  rewrite > (S_pred a) in H1
+  [ apply False_ind.
+    apply (eq_to_not_lt O ((S (pred a))*(S m)))
+    [ apply sym_eq.
+      assumption
+    | apply lt_O_times_S_S
+    ]
+  | assumption
+  ]
+]
+qed.
+
+theorem O_lt_times_to_O_lt: \forall a,c:nat.
+O \lt (a * c) \to O \lt a.
+intros.
+apply (nat_case1 a)
+[ intros.
+  rewrite > H1 in H.
+  simplify in H.
+  assumption
+| intros.
+  apply lt_O_S
+]
+qed.
+
 (* times *)
 theorem monotonic_lt_times_r: 
 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
@@ -77,6 +127,20 @@ simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
 apply lt_plus.assumption.assumption.
 qed.
 
+(* a simple variant of the previus monotionic_lt_times *)
+theorem monotonic_lt_times_variant: \forall c:nat.
+O \lt c \to monotonic nat lt (\lambda t.(t*c)).
+intros.
+apply (increasing_to_monotonic).
+unfold increasing.
+intros.
+simplify.
+rewrite > sym_plus.
+rewrite > plus_n_O in \vdash (? % ?).
+apply lt_plus_r.
+assumption.
+qed.
+
 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 \def monotonic_lt_times_r.
 
@@ -236,6 +300,7 @@ apply (trans_lt ? (S O)).
 unfold lt. apply le_n.assumption.
 qed.
 
+
 (* general properties of functions *)
 theorem monotonic_to_injective: \forall f:nat\to nat.
 monotonic nat lt f \to injective nat nat f.
diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index f1178107a..11585f206 100644
--- a/matita/library/nat/minus.ma
+++ b/matita/library/nat/minus.ma
@@ -287,6 +287,15 @@ rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
+theorem lt_O_minus_to_lt: \forall a,b:nat.
+O \lt b-a \to a \lt b.
+intros.
+rewrite > (plus_n_O a).
+rewrite > (sym_plus a O).
+apply (lt_minus_to_plus O  a b).
+assumption.
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.
diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 3257e2e1a..8053d50de 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -139,6 +139,19 @@ apply Hcut.assumption.rewrite < H1.
 apply not_le_Sn_n.
 qed.
 
+(*not lt*)
+theorem eq_to_not_lt: \forall a,b:nat.
+a = b \to a \nlt b.
+intros.
+unfold Not.
+intros.
+rewrite > H in H1.
+apply (lt_to_not_eq b b)
+[ assumption
+| reflexivity
+]
+qed.
+
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
 simplify.intros.unfold lt in H.elim H.
diff --git a/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma b/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
new file mode 100644
index 000000000..6a5fc2058
--- /dev/null
+++ b/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
@@ -0,0 +1,488 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.
+elim H
+[ simplify.
+  apply (lt_O_S O)
+| rewrite < (pred_Sn n1).
+  apply (lt_to_le_to_lt O (S (S O)) n1)
+  [ apply le_S.
+    apply (le_n (S O))
+  | assumption
+  ]
+]
+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 (O = n \mod m)
+[ rewrite > Hcut.
+  apply div_mod.
+  assumption
+| apply sym_eq.
+  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 (? % ?)
+  [ rewrite < (sym_times a c).
+    apply (O_lt_const_to_le_times_const).
+    assumption
+  | assumption
+  | assumption
+  ]
+]
+qed.
+
+
+theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
+O \lt b \to (b*c) \le a \to c \le (a /b).
+intros.
+rewrite > (div_mod a b) in H1
+[ apply (le_times_to_le b ? ?)
+  [ assumption
+  | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
+    [ elim Hcut
+      [ rewrite < (sym_times c b).
+        rewrite < (sym_times (a/b) b).
+        assumption
+      | cut (a/b \lt c)
+        [ change in Hcut1 with ((S (a/b)) \le c).
+          cut( b*(S (a/b)) \le b*c)
+          [ rewrite > (sym_times b (S (a/b))) in Hcut2.
+            simplify in Hcut2.
+            cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
+            [ cut (b \le (a \mod b))
+              [ apply False_ind.
+                apply (lt_to_not_le (a \mod b) b)
+                [ apply (lt_mod_m_m).
+                  assumption
+                | assumption
+                ]
+              | apply (le_plus_to_le ((a/b)*b)).
+                rewrite > sym_plus.
+                assumption.
+              ]
+            | apply (trans_le ? (b*c) ?);
+                assumption
+            ]
+          | apply (le_times_r b ? ?).
+            assumption
+          ]
+        | apply (lt_times_n_to_lt b (a/b) c)
+          [ assumption
+          | assumption
+          ]
+        ]
+      ]
+    | apply (leb_elim (c*b) ((a/b)*b))
+      [ intros.
+        left.
+        assumption
+      | intros.
+        right.
+        apply cic:/matita/nat/orders/not_le_to_lt.con. 
+        assumption        
+      ]
+    ]
+  ]
+| assumption
+] 
+qed.
+
+theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
+\forall a,b:nat.
+O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
+intros.
+elim H2.
+cut (O \lt n2)
+[ rewrite > H3.
+  rewrite > (sym_times a n2).
+  rewrite > (div_times_ltO n2 a);
+    assumption  
+| apply (divides_to_lt_O n2 b)
+  [ assumption
+  | apply (witness n2 b a).
+    rewrite > sym_times.
+    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_times_to_eqSO: \forall a,d:nat.
+O \lt d \to a*d = d \to a = (S O).
+intros.
+rewrite > (plus_n_O d) in H1:(? ? ? %).
+cut (a*d -d = O)
+[ rewrite  > sym_times in Hcut.
+  rewrite > times_n_SO in Hcut:(? ? (? ? %) ?).
+  rewrite < distr_times_minus in Hcut.
+  cut ((a - (S O)) = O)
+  [ apply (minus_to_plus a (S O) O)
+    [ apply (nat_case1 a)
+      [ intros.
+        rewrite > H2 in H1.
+        simplify in H1.
+        rewrite < (plus_n_O d) in H1.
+        rewrite < H1 in H.
+        apply False_ind.
+        change in H with ((S O) \le O).
+        apply (not_le_Sn_O O H)
+      | intros.
+        apply (le_S_S O m).
+        apply (le_O_n m)
+      ]
+    | assumption
+    ]
+  | apply (lt_times_eq_O d (a - (S O)));
+      assumption
+  ]
+| apply (plus_to_minus ).
+  assumption
+]
+qed.
+
+theorem div_mod_minus:
+\forall a,b:nat. O \lt b \to
+(a /b)*b = a - (a \mod b).
+intros.
+apply sym_eq.
+apply (inj_plus_r (a \mod b)).
+rewrite > (sym_plus (a \mod b) ?).
+rewrite < (plus_minus_m_m a (a \mod b))
+[ rewrite > sym_plus.
+  apply div_mod.
+  assumption
+| rewrite > (div_mod a b) in \vdash (? ? %)
+  [ rewrite > plus_n_O in \vdash (? % ?).
+    rewrite > sym_plus.
+    apply cic:/matita/nat/le_arith/le_plus_n.con
+  | assumption
+  ]
+]
+qed.
+
+theorem sum_div_eq_div: \forall a,b,c:nat.
+O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
+intros.
+elim H2.
+rewrite > H3.
+rewrite > (sym_times c n2).
+rewrite > (div_plus_times c n2 b)
+[ rewrite > (div_times_ltO n2 c)
+  [ reflexivity
+  | assumption
+  ]
+| assumption
+]
+qed.
+
+
+(* A corollary to the division theorem (between natural numbers).
+ *
+ * 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_minus
+  [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b))
+    [ rewrite < (sym_plus a b).
+      rewrite > (eq_minus_plus_plus_minus a b (a \mod b))
+      [ rewrite > (plus_n_O a) in \vdash (? % ?).
+        apply (le_to_lt_to_plus_lt)
+        [ apply (le_n a)
+        | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con.      
+          apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con.
+          assumption
+        ]
+      | apply lt_to_le.
+        apply lt_mod_m_m.
+        assumption
+      ]
+    | rewrite > (div_mod a b) in \vdash (? ? %)
+      [ rewrite > plus_n_O in \vdash (? % ?).
+        rewrite > sym_plus.
+        apply cic:/matita/nat/le_arith/le_plus_n.con
+      | assumption
+      ]
+    ]
+  | assumption
+  ]
+]
+qed.
+
+theorem th_div_interi_1: \forall a,c,b:nat.
+O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
+intros.
+apply (le_to_le_to_eq)
+[ cut (a/b \le c \lor c \lt a/b)
+  [ elim Hcut
+    [ assumption
+    | change in H3 with ((S c) \le (a/b)).
+      cut (b*(S c) \le (b*(a/b)))
+      [ rewrite > (sym_times b (S c)) in Hcut1.
+        cut (a \lt (b * (a/b)))
+        [ rewrite > (div_mod a b) in Hcut2:(? % ?)
+          [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %).
+            cut ((a \mod b) \lt O)
+            [ apply False_ind.
+              apply (lt_to_not_le (a \mod b) O)
+              [ assumption
+              | apply le_O_n
+              ]              
+            | apply (lt_plus_to_lt_r ((a/b)*b)).
+              rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)).
+              assumption 
+            ]
+          | assumption
+          ]
+        | apply (lt_to_le_to_lt ? (b*(S c)) ?)
+          [ assumption
+          | rewrite > (sym_times b (S c)).
+            assumption
+          ]
+        ]
+      | apply le_times_r.
+        assumption
+      ]
+    ]
+  | apply (leb_elim (a/b) c)
+    [ intros.
+      left.
+      assumption
+    | intros.
+      right.
+      apply cic:/matita/nat/orders/not_le_to_lt.con. 
+      assumption
+    ]
+  ] 
+| apply (bTIMESc_le_a_to_c_le_aDIVb);
+    assumption
+]
+qed.
+
+theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
+O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
+intros.
+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.
+
+
+
+
+
+
+
+
+
+
+