From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 16 Mar 2007 08:04:32 +0000 (+0000)
Subject: Extensions required for the moebius function (in Z).
X-Git-Tag: 0.4.95@7852~564
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e95f5d784fe7830fe9ed10b3e782ef2206fea896;p=helm.git

Extensions required for the moebius function (in Z).
---

diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma
index ccddcca3f..65ba0e9e5 100644
--- a/matita/library/nat/div_and_mod.ma
+++ b/matita/library/nat/div_and_mod.ma
@@ -193,6 +193,25 @@ unfold lt.apply le_S_S.apply le_O_n.
 rewrite < plus_n_O.rewrite < sym_times.reflexivity.
 qed.
 
+lemma div_plus_times: \forall m,q,r:nat. r < m \to  (q*m+r)/ m = q. 
+intros.
+apply (div_mod_spec_to_eq (q*m+r) m ? ((q*m+r) \mod m) ? r)
+  [apply div_mod_spec_div_mod.
+   apply (le_to_lt_to_lt ? r)
+    [apply le_O_n|assumption]
+  |apply div_mod_spec_intro[assumption|reflexivity]
+  ]
+qed.
+
+lemma mod_plus_times: \forall m,q,r:nat. r < m \to  (q*m+r) \mod m = r. 
+intros.
+apply (div_mod_spec_to_eq2 (q*m+r) m ((q*m+r)/ m) ((q*m+r) \mod m) q r)
+  [apply div_mod_spec_div_mod.
+   apply (le_to_lt_to_lt ? r)
+    [apply le_O_n|assumption]
+  |apply div_mod_spec_intro[assumption|reflexivity]
+  ]
+qed.
 (* some properties of div and mod *)
 theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
 intros.
diff --git a/matita/library/nat/euler_theorem.ma b/matita/library/nat/euler_theorem.ma
index d58f7c2b0..43638fca6 100644
--- a/matita/library/nat/euler_theorem.ma
+++ b/matita/library/nat/euler_theorem.ma
@@ -17,7 +17,46 @@ 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
+  [simplify.rewrite > H. reflexivity
+  |simplify.
+   rewrite < plus_n_O.
+   apply eq_f.assumption
+  ]
+qed.
+
+lemma count_card1: \forall p.\forall n.
+p O = false \to p n = false \to count n p = card n p.
+intros 3.apply (nat_case n)
+  [intro.simplify.rewrite > H. reflexivity
+  |intros.rewrite > (count_card ? ? H).
+   simplify.rewrite > H1.reflexivity
+  ]
+qed.
+ 
+
 (* 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)).
 intro.apply (nat_case n)
diff --git a/matita/library/nat/exp.ma b/matita/library/nat/exp.ma
index e40844e3f..c69be6b5f 100644
--- a/matita/library/nat/exp.ma
+++ b/matita/library/nat/exp.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/exp".
 
 include "nat/div_and_mod.ma".
+include "nat/lt_arith.ma".
 
 let rec exp n m on m\def 
  match m with 
@@ -95,3 +96,51 @@ qed.
 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
 p \sup n = p \sup m \to n = m \def
 injective_exp_r.
+
+theorem le_exp: \forall n,m,p:nat. O < p \to n \le m \to exp p n \le exp p m.
+apply nat_elim2
+  [intros.
+   apply lt_O_exp.assumption
+  |intros.
+   apply False_ind.
+   apply (le_to_not_lt ? ? ? H1).
+   apply le_O_n
+  |intros.
+   simplify.
+   apply le_times
+    [apply le_n
+    |apply H[assumption|apply le_S_S_to_le.assumption]
+    ]
+  ]
+qed.
+ 
+theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
+apply nat_elim2
+  [intros.
+   apply (lt_O_n_elim ? H1).intro.
+   simplify.unfold lt.
+   rewrite > times_n_SO.
+   apply le_times
+    [assumption
+    |apply lt_O_exp.
+     apply (trans_lt ? (S O))[apply le_n|assumption]
+    ]
+  |intros.
+   apply False_ind.
+   apply (le_to_not_lt ? ? ? H1).
+   apply le_O_n
+  |intros.simplify.
+   apply lt_times_r1
+    [apply (trans_lt ? (S O))[apply le_n|assumption]
+    |apply H
+      [apply H1
+      |apply le_S_S_to_le.assumption
+      ]
+    ]
+  ]
+qed.
+
+     
+   
+   
+   
\ No newline at end of file
diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 85351c06d..37a704592 100644
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -27,10 +27,10 @@ definition max_prime_factor \def \lambda n:nat.
 theorem divides_max_prime_factor_n:
   \forall n:nat. (S O) < n
   \to nth_prime (max_prime_factor n) \divides n.
-intros; apply divides_b_true_to_divides;
-[ apply lt_O_nth_prime_n;
-| apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
-  cut (\exists i. nth_prime i = smallest_factor n);
+intros.
+apply divides_b_true_to_divides.
+apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
+cut (\exists i. nth_prime i = smallest_factor n);
   [ elim Hcut.
     apply (ex_intro nat ? a);
     split;
@@ -56,7 +56,7 @@ intros; apply divides_b_true_to_divides;
     (* 
     apply prime_to_nth_prime;
     apply prime_smallest_factor_n;
-    assumption; *) ] ]
+    assumption; *) ] 
 qed.
 
 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to 
@@ -90,6 +90,17 @@ auto.
 *)  
 qed.
 
+theorem divides_to_max_prime_factor1 : \forall n,m. O < n \to O < m \to n \divides m \to 
+max_prime_factor n \le max_prime_factor m.
+intros 3.
+elim (le_to_or_lt_eq ? ? H)
+  [apply divides_to_max_prime_factor
+    [assumption|assumption|assumption]
+  |rewrite < H1.
+   simplify.apply le_O_n.
+  ]
+qed.
+
 theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
 p = max_prime_factor n \to 
 (pair nat nat q r) = p_ord n (nth_prime p) \to
diff --git a/matita/library/nat/iteration2.ma b/matita/library/nat/iteration2.ma
new file mode 100644
index 000000000..0c3091d30
--- /dev/null
+++ b/matita/library/nat/iteration2.ma
@@ -0,0 +1,683 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/iteration2.ma".
+
+include "nat/primes.ma".
+include "nat/ord.ma".
+
+let rec sigma_p n p (g:nat \to nat) \def
+  match n with
+   [ O \Rightarrow O
+   | (S k) \Rightarrow 
+      match p k with
+      [true \Rightarrow (g k)+(sigma_p k p g)
+      |false \Rightarrow sigma_p k p g]
+   ].
+   
+theorem true_to_sigma_p_Sn: 
+\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
+p n = true \to sigma_p (S n) p g = 
+(g n)+(sigma_p n p g).
+intros.simplify.
+rewrite > H.reflexivity.
+qed.
+   
+theorem false_to_sigma_p_Sn: 
+\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
+p n = false \to sigma_p (S n) p g = sigma_p n p g.
+intros.simplify.
+rewrite > H.reflexivity.
+qed.
+
+theorem eq_sigma_p: \forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to nat.\forall n.
+(\forall x.  x < n \to p1 x = p2 x) \to
+(\forall x.  x < n \to g1 x = g2 x) \to
+sigma_p n p1 g1 = sigma_p n p2 g2.
+intros 5.elim n
+  [reflexivity
+  |apply (bool_elim ? (p1 n1))
+    [intro.
+     rewrite > (true_to_sigma_p_Sn ? ? ? H3).
+     rewrite > true_to_sigma_p_Sn
+      [apply eq_f2
+        [apply H2.apply le_n.
+        |apply H
+          [intros.apply H1.apply le_S.assumption
+          |intros.apply H2.apply le_S.assumption
+          ]
+        ]
+      |rewrite < H3.apply sym_eq.apply H1.apply le_n
+      ]
+    |intro.
+     rewrite > (false_to_sigma_p_Sn ? ? ? H3).
+     rewrite > false_to_sigma_p_Sn
+      [apply H
+        [intros.apply H1.apply le_S.assumption
+        |intros.apply H2.apply le_S.assumption
+        ]
+      |rewrite < H3.apply sym_eq.apply H1.apply le_n
+      ]
+    ]
+  ]
+qed.
+
+theorem sigma_p_false: 
+\forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
+intros.
+elim n[reflexivity|simplify.assumption]
+qed.
+
+theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
+\forall g: nat \to nat.
+sigma_p (k+n) p g 
+= sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
+intros.
+elim k
+  [reflexivity
+  |apply (bool_elim ? (p (n1+n)))
+    [intro.
+     simplify in \vdash (? ? (? % ? ?) ?).    
+     rewrite > (true_to_sigma_p_Sn ? ? ? H1).
+     rewrite > (true_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1).
+     rewrite > assoc_plus.
+     rewrite < H.reflexivity
+    |intro.
+     simplify in \vdash (? ? (? % ? ?) ?).    
+     rewrite > (false_to_sigma_p_Sn ? ? ? H1).
+     rewrite > (false_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1).
+     assumption.
+    ]
+  ]
+qed.
+
+theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
+\forall p:nat \to bool.
+\forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
+p i = false) \to sigma_p m p g = sigma_p n p g.
+intros 5.
+elim H
+  [reflexivity
+  |simplify.
+   rewrite > H3
+    [simplify.
+     apply H2.
+     intros.
+     apply H3[apply H4|apply le_S.assumption]
+    |assumption
+    |apply le_n
+    ]
+  ]
+qed.
+
+theorem sigma_p2 : 
+\forall n,m:nat.
+\forall p1,p2:nat \to bool.
+\forall g: nat \to nat \to nat.
+sigma_p (n*m) 
+  (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) 
+  (\lambda x.g (div x m) (mod x m)) =
+sigma_p n p1 
+  (\lambda x.sigma_p m p2 (g x)).
+intros.
+elim n
+  [simplify.reflexivity
+  |apply (bool_elim ? (p1 n1))
+    [intro.
+     rewrite > (true_to_sigma_p_Sn ? ? ? H1).
+     simplify in \vdash (? ? (? % ? ?) ?);
+     rewrite > sigma_p_plus.
+     rewrite < H.
+     apply eq_f2
+      [apply eq_sigma_p
+        [intros.
+         rewrite > sym_plus.
+         rewrite > (div_plus_times ? ? ? H2).
+         rewrite > (mod_plus_times ? ? ? H2).
+         rewrite > H1.
+         simplify.reflexivity
+        |intros.
+         rewrite > sym_plus.
+         rewrite > (div_plus_times ? ? ? H2).
+         rewrite > (mod_plus_times ? ? ? H2).
+         rewrite > H1.
+         simplify.reflexivity.   
+        ]
+      |reflexivity
+      ]
+    |intro.
+     rewrite > (false_to_sigma_p_Sn ? ? ? H1).
+     simplify in \vdash (? ? (? % ? ?) ?);
+     rewrite > sigma_p_plus.
+     rewrite > H.
+     apply (trans_eq ? ? (O+(sigma_p n1 p1 (\lambda x:nat.sigma_p m p2 (g x)))))
+      [apply eq_f2
+        [rewrite > (eq_sigma_p ? (\lambda x.false) ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
+          [apply sigma_p_false
+          |intros.
+           rewrite > sym_plus.
+           rewrite > (div_plus_times ? ? ? H2).
+           rewrite > (mod_plus_times ? ? ? H2).
+           rewrite > H1.
+           simplify.reflexivity
+          |intros.reflexivity.
+          ]
+        |reflexivity
+        ]
+      |reflexivity   
+      ]
+    ]
+  ]
+qed.
+
+lemma sigma_p_gi: \forall g: nat \to nat.
+\forall n,i.\forall p:nat \to bool.i < n \to p i = true \to 
+sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
+intros 2.
+elim n
+  [apply False_ind.
+   apply (not_le_Sn_O i).
+   assumption
+  |apply (bool_elim ? (p n1));intro
+    [elim (le_to_or_lt_eq i n1)
+      [rewrite > true_to_sigma_p_Sn
+        [rewrite > true_to_sigma_p_Sn
+          [rewrite < assoc_plus.
+           rewrite < sym_plus in \vdash (? ? ? (? % ?)).
+           rewrite > assoc_plus.
+           apply eq_f2
+            [reflexivity
+            |apply H[assumption|assumption]
+            ]
+          |rewrite > H3.simplify.
+           change with (notb (eqb n1 i) = notb false).
+           apply eq_f.
+           apply not_eq_to_eqb_false.
+           unfold Not.intro.
+           apply (lt_to_not_eq ? ? H4).
+           apply sym_eq.assumption
+          ]
+        |assumption
+        ]
+      |rewrite > true_to_sigma_p_Sn
+        [rewrite > H4.
+         apply eq_f2
+          [reflexivity
+          |rewrite > false_to_sigma_p_Sn
+            [apply eq_sigma_p
+              [intros.
+               elim (p x)
+                [simplify.
+                 change with (notb false = notb (eqb x n1)).
+                 apply eq_f.
+                 apply sym_eq. 
+                 apply not_eq_to_eqb_false.
+                 apply (lt_to_not_eq ? ? H5)
+                |reflexivity
+                ]
+              |intros.reflexivity
+              ]
+            |rewrite > H3.
+             rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
+             reflexivity
+            ]
+          ]
+        |assumption
+        ]
+      |apply le_S_S_to_le.assumption
+      ]
+    |rewrite > false_to_sigma_p_Sn
+      [elim (le_to_or_lt_eq i n1)
+        [rewrite > false_to_sigma_p_Sn
+          [apply H[assumption|assumption]
+          |rewrite > H3.reflexivity
+          ]
+        |apply False_ind. 
+         apply not_eq_true_false.
+         rewrite < H2.
+         rewrite > H4.
+         assumption
+        |apply le_S_S_to_le.assumption
+        ]
+      |assumption
+      ]
+    ] 
+  ] 
+qed.
+
+theorem eq_sigma_p_gh: 
+\forall g,h,h1: nat \to nat.\forall n,n1.
+\forall p1,p2:nat \to bool.
+(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
+(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
+(\forall i. i < n \to p1 i = true \to h i < n1) \to 
+(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
+(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
+(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
+sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
+intros 4.
+elim n
+  [generalize in match H5.
+   elim n1
+    [reflexivity
+    |apply (bool_elim ? (p2 n2));intro
+      [apply False_ind.
+       apply (not_le_Sn_O (h1 n2)).
+       apply H7
+        [apply le_n|assumption]
+      |rewrite > false_to_sigma_p_Sn
+        [apply H6.
+         intros.  
+            apply H7[apply le_S.apply H9|assumption]
+        |assumption
+        ]
+      ]
+    ]
+  |apply (bool_elim ? (p1 n1));intro
+    [rewrite > true_to_sigma_p_Sn
+      [rewrite > (sigma_p_gi g n2 (h n1))
+        [apply eq_f2
+          [reflexivity
+          |apply H
+            [intros.
+             rewrite > H1
+              [simplify.
+               change with ((\not eqb (h i) (h n1))= \not false).
+               apply eq_f.
+               apply not_eq_to_eqb_false.
+               unfold Not.intro.
+               apply (lt_to_not_eq ? ? H8).
+               rewrite < H2
+                [rewrite < (H2 n1)
+                  [apply eq_f.assumption|apply le_n|assumption]
+                |apply le_S.assumption
+                |assumption
+                ]
+              |apply le_S.assumption
+              |assumption
+              ]
+            |intros.
+             apply H2[apply le_S.assumption|assumption]
+            |intros.
+             apply H3[apply le_S.assumption|assumption]
+            |intros.
+             apply H4
+              [assumption
+              |generalize in match H9.
+               elim (p2 j)
+                [reflexivity|assumption]
+              ]
+            |intros.
+             apply H5
+              [assumption
+              |generalize in match H9.
+               elim (p2 j)
+                [reflexivity|assumption]
+              ]
+            |intros.
+             elim (le_to_or_lt_eq (h1 j) n1)
+              [assumption
+              |generalize in match H9.
+               elim (p2 j)
+                [simplify in H11.
+                 absurd (j = (h n1))
+                  [rewrite < H10.
+                   rewrite > H5
+                    [reflexivity|assumption|auto]
+                  |apply eqb_false_to_not_eq.
+                   generalize in match H11.
+                   elim (eqb j (h n1))
+                    [apply sym_eq.assumption|reflexivity]
+                  ]
+                |simplify in H11.
+                 apply False_ind.
+                 apply not_eq_true_false.
+                 apply sym_eq.assumption
+                ]
+              |apply le_S_S_to_le.
+               apply H6
+                [assumption
+                |generalize in match H9.
+                 elim (p2 j)
+                  [reflexivity|assumption]
+                ]
+              ]
+            ]
+          ]
+        |apply H3[apply le_n|assumption]
+        |apply H1[apply le_n|assumption]
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_sigma_p_Sn
+     [apply H
+       [intros.apply H1[apply le_S.assumption|assumption]
+       |intros.apply H2[apply le_S.assumption|assumption]
+       |intros.apply H3[apply le_S.assumption|assumption]
+       |intros.apply H4[assumption|assumption]
+       |intros.apply H5[assumption|assumption]
+       |intros.
+        elim (le_to_or_lt_eq (h1 j) n1)
+          [assumption
+          |absurd (j = (h n1))
+            [rewrite < H10.
+             rewrite > H5
+               [reflexivity|assumption|assumption]
+            |unfold Not.intro.
+             apply not_eq_true_false.
+             rewrite < H7.
+             rewrite < H10.
+             rewrite > H4
+              [reflexivity|assumption|assumption]
+            ]
+          |apply le_S_S_to_le.
+           apply H6[assumption|assumption]
+          ]
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+definition p_ord_times \def
+\lambda p,m,x.
+  match p_ord x p with
+  [pair q r \Rightarrow r*m+q].
+  
+theorem  eq_p_ord_times: \forall p,m,x.
+p_ord_times p m x = (ord_rem x p)*m+(ord x p).
+intros.unfold p_ord_times. unfold ord_rem.
+unfold ord.
+elim (p_ord x p).
+reflexivity.
+qed.
+
+theorem div_p_ord_times: 
+\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
+intros.rewrite > eq_p_ord_times.
+apply div_plus_times.
+assumption.
+qed.
+
+theorem mod_p_ord_times: 
+\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
+intros.rewrite > eq_p_ord_times.
+apply mod_plus_times.
+assumption.
+qed.
+
+theorem sigma_p_divides: 
+\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
+\forall g: nat \to nat.
+sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
+sigma_p (S n) (\lambda x.divides_b x n)
+  (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
+intros.
+cut (O < p)
+  [rewrite < sigma_p2.
+   apply (trans_eq ? ? 
+    (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n)
+       (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))))
+    [apply sym_eq.
+     apply (eq_sigma_p_gh g ? (p_ord_times p (S m)))
+      [intros.
+       lapply (divides_b_true_to_lt_O ? ? H H4).
+       apply divides_to_divides_b_true
+        [rewrite > (times_n_O O).
+         apply lt_times
+          [assumption
+          |apply lt_O_exp.assumption
+          ]
+        |apply divides_times
+          [apply divides_b_true_to_divides.assumption
+          |apply (witness ? ? (p \sup (m-i \mod (S m)))).
+           rewrite < exp_plus_times.
+           apply eq_f.
+           rewrite > sym_plus.
+           apply plus_minus_m_m.
+           auto
+          ]
+        ]
+      |intros.
+       lapply (divides_b_true_to_lt_O ? ? H H4).
+       unfold p_ord_times.
+       rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
+        [change with ((i/S m)*S m+i \mod S m=i).
+         apply sym_eq.
+         apply div_mod.
+         apply lt_O_S
+        |assumption
+        |unfold Not.intro.
+         apply H2.
+         apply (trans_divides ? (i/ S m))
+          [assumption|
+           apply divides_b_true_to_divides;assumption]
+        |apply sym_times.
+        ]
+      |intros.
+       apply le_S_S.
+       apply le_times
+        [apply le_S_S_to_le.
+         change with ((i/S m) < S n).
+         apply (lt_times_to_lt_l m).
+         apply (le_to_lt_to_lt ? i)
+          [auto|assumption]
+        |apply le_exp
+          [assumption
+          |apply le_S_S_to_le.
+           apply lt_mod_m_m.
+           apply lt_O_S
+          ]
+        ]
+      |intros.
+       cut (ord j p < S m)
+        [rewrite > div_p_ord_times
+          [apply divides_to_divides_b_true
+            [apply lt_O_ord_rem
+             [elim H1.assumption
+             |apply (divides_b_true_to_lt_O ? ? ? H4).
+               rewrite > (times_n_O O).
+               apply lt_times
+               [assumption|apply lt_O_exp.assumption]
+             ]
+           |cut (n = ord_rem (n*(exp p m)) p)
+              [rewrite > Hcut2.
+               apply divides_to_divides_ord_rem
+                [apply (divides_b_true_to_lt_O ? ? ? H4).
+                 rewrite > (times_n_O O).
+                 apply lt_times
+                 [assumption|apply lt_O_exp.assumption]
+                 |rewrite > (times_n_O O).
+                   apply lt_times
+                  [assumption|apply lt_O_exp.assumption]
+               |assumption
+               |apply divides_b_true_to_divides.
+                assumption
+               ]
+              |unfold ord_rem.
+              rewrite > (p_ord_exp1 p ? m n)
+                [reflexivity
+               |assumption
+                |assumption
+               |apply sym_times
+               ]
+             ]
+            ]
+          |assumption
+          ]
+        |cut (m = ord (n*(exp p m)) p)
+          [apply le_S_S.
+           rewrite > Hcut1.
+           apply divides_to_le_ord
+            [apply (divides_b_true_to_lt_O ? ? ? H4).
+             rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          |unfold ord.
+           rewrite > (p_ord_exp1 p ? m n)
+            [reflexivity
+            |assumption
+            |assumption
+            |apply sym_times
+            ]
+          ]
+        ]
+      |intros.
+       cut (ord j p < S m)
+        [rewrite > div_p_ord_times
+          [rewrite > mod_p_ord_times
+            [rewrite > sym_times.
+             apply sym_eq.
+             apply exp_ord
+              [elim H1.assumption
+              |apply (divides_b_true_to_lt_O ? ? ? H4).
+               rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              ]
+           |cut (m = ord (n*(exp p m)) p)
+             [apply le_S_S.
+              rewrite > Hcut2.
+              apply divides_to_le_ord
+               [apply (divides_b_true_to_lt_O ? ? ? H4).
+                rewrite > (times_n_O O).
+                apply lt_times
+                 [assumption|apply lt_O_exp.assumption]
+               |rewrite > (times_n_O O).
+                apply lt_times
+                 [assumption|apply lt_O_exp.assumption]
+               |assumption
+               |apply divides_b_true_to_divides.
+                assumption
+               ]
+             |unfold ord.
+              rewrite > (p_ord_exp1 p ? m n)
+                [reflexivity
+                |assumption
+                |assumption
+                |apply sym_times
+                ]
+              ]
+            ]
+          |assumption
+          ]
+        |cut (m = ord (n*(exp p m)) p)
+          [apply le_S_S.
+           rewrite > Hcut1.
+           apply divides_to_le_ord
+            [apply (divides_b_true_to_lt_O ? ? ? H4).
+             rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          |unfold ord.
+           rewrite > (p_ord_exp1 p ? m n)
+            [reflexivity
+            |assumption
+            |assumption
+            |apply sym_times
+            ]
+          ]
+        ]
+      |intros.
+       rewrite > eq_p_ord_times.
+       rewrite > sym_plus.
+       apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
+        [apply lt_plus_l.
+         apply le_S_S.
+         cut (m = ord (n*(p \sup m)) p)
+          [rewrite > Hcut1.
+           apply divides_to_le_ord
+            [apply (divides_b_true_to_lt_O ? ? ? H4).
+             rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          |unfold ord.
+           rewrite > sym_times.
+           rewrite > (p_ord_exp1 p ? m n)
+            [reflexivity
+            |assumption
+            |assumption
+            |reflexivity
+            ]
+          ]
+        |change with (S (ord_rem j p)*S m \le S n*S m).
+         apply le_times_l.
+         apply le_S_S.
+         cut (n = ord_rem (n*(p \sup m)) p)
+          [rewrite > Hcut1.
+           apply divides_to_le
+            [apply lt_O_ord_rem
+              [elim H1.assumption
+              |rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              ]
+            |apply divides_to_divides_ord_rem
+              [apply (divides_b_true_to_lt_O ? ? ? H4).
+               rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              |rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              |assumption
+              |apply divides_b_true_to_divides.
+               assumption
+              ]
+            ]
+        |unfold ord_rem.
+         rewrite > sym_times.
+         rewrite > (p_ord_exp1 p ? m n)
+          [reflexivity
+          |assumption
+          |assumption
+          |reflexivity
+          ]
+        ]
+      ]
+    ]
+  |apply eq_sigma_p
+    [intros.
+     elim (divides_b (x/S m) n);reflexivity
+    |intros.reflexivity
+    ]
+  ]
+|elim H1.apply lt_to_le.assumption
+]
+qed.
+    
+
diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma
index 6635a8b0d..b01bd5461 100644
--- a/matita/library/nat/lt_arith.ma
+++ b/matita/library/nat/lt_arith.ma
@@ -111,6 +111,28 @@ assumption.
 apply (ltn_to_ltO p q H2).
 qed.
 
+theorem lt_times_r1: 
+\forall n,m,p. O < n \to m < p \to n*m < n*p.
+intros.
+elim H;apply lt_times_r;assumption.
+qed.
+
+theorem lt_times_l1: 
+\forall n,m,p. O < n \to m < p \to m*n < p*n.
+intros.
+elim H;apply lt_times_l;assumption.
+qed.
+
+theorem lt_to_le_to_lt_times : 
+\forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
+intros.
+apply (le_to_lt_to_lt ? (n*m1))
+  [apply le_times_r.assumption
+  |apply lt_times_l1
+    [assumption|assumption]
+  ]
+qed.
+
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
diff --git a/matita/library/nat/minimization.ma b/matita/library/nat/minimization.ma
index 0abed5ad3..2d273e180 100644
--- a/matita/library/nat/minimization.ma
+++ b/matita/library/nat/minimization.ma
@@ -72,11 +72,6 @@ intro.simplify.rewrite < H3.
 rewrite > H2.simplify.apply le_n.
 qed.
 
-
-definition max_spec \def \lambda f:nat \to bool.\lambda n: nat.
-\exists i. (le i n) \land (f i = true) \to
-(f n) = true \land (\forall i. i < n \to (f i = false)).
-
 theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
 (\exists i:nat. le i n \land f i = true) \to f (max n f) = true. 
 intros 2.
@@ -119,6 +114,52 @@ apply le_S_S_to_le.assumption.
 intro.rewrite > H7.assumption.
 qed.
 
+definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat.
+m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)).
+
+theorem max_spec_to_max: \forall f:nat \to bool.\forall n,m:nat.
+max_spec f n m \to max n f = m.
+intros 2.
+elim n
+  [elim H.elim H1.apply (le_n_O_elim ? H3).
+   apply max_O_f
+  |elim H1.
+   elim (max_S_max f n1)
+    [elim H4.
+     rewrite > H6.
+     apply le_to_le_to_eq
+      [apply not_lt_to_le.
+       unfold Not.intro.
+       apply not_eq_true_false.
+       rewrite < H5.
+       apply H3
+        [assumption|apply le_n]
+      |elim H2.assumption
+      ]
+    |elim H4.
+     rewrite > H6.
+     apply H.
+     elim H2.
+     split
+      [split
+        [elim (le_to_or_lt_eq ? ? H7)
+          [apply le_S_S_to_le.assumption
+          |apply False_ind.
+           apply not_eq_true_false.
+           rewrite < H8.
+           rewrite > H9.
+           assumption
+          ]
+        |assumption
+        ]
+      |intros.
+       apply H3
+        [assumption|apply le_S.assumption]
+      ]
+    ]
+  ]
+qed.
+ 
 let rec min_aux off n f \def
   match f (n-off) with 
   [ true \Rightarrow (n-off)
diff --git a/matita/library/nat/nth_prime.ma b/matita/library/nat/nth_prime.ma
index e174266e6..9d01e99f2 100644
--- a/matita/library/nat/nth_prime.ma
+++ b/matita/library/nat/nth_prime.ma
@@ -159,6 +159,17 @@ intros.apply (trans_lt O (S O)).
 unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 qed.
 
+theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
+intro.
+elim n
+  [apply lt_O_nth_prime_n
+  |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
+    [unfold.apply le_S_S.assumption
+    |apply lt_nth_prime_n_nth_prime_Sn
+    ]
+  ]
+qed.
+
 theorem ex_m_le_n_nth_prime_m: 
 \forall n: nat. nth_prime O \le n \to 
 \exists m. nth_prime m \le n \land n < nth_prime (S m).
diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index b7d02f87f..159e8613b 100644
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -19,8 +19,6 @@ include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/relevant_equations.ma". (* required by auto paramod *)
 
-(* this definition of log is based on pairs, with a remainder *)
-
 let rec p_ord_aux p n m \def
   match n \mod m with
   [ O \Rightarrow 
@@ -240,4 +238,204 @@ apply le_to_not_lt.
 apply divides_to_le.unfold.apply le_n.assumption.
 rewrite < times_n_SO.
 apply exp_n_SO.
-qed.
\ No newline at end of file
+qed.
+
+(* spostare *)
+theorem le_plus_to_le: 
+\forall a,n,m. a + n \le a + m \to n \le m.
+intro.
+elim a
+  [assumption
+  |apply H.
+   apply le_S_S_to_le.assumption
+  ]
+qed.
+  
+theorem le_times_to_le: 
+\forall a,n,m. O < a \to a * n \le a * m \to n \le m.
+intro.
+apply nat_elim2;intros
+  [apply le_O_n
+  |apply False_ind.
+   rewrite < times_n_O in H1.
+   generalize in match H1.
+   apply (lt_O_n_elim ? H).
+   intros.
+   simplify in H2.
+   apply (le_to_not_lt ? ? H2).
+   apply lt_O_S
+  |apply le_S_S.
+   apply H
+    [assumption
+    |rewrite < times_n_Sm in H2.
+     rewrite < times_n_Sm in H2.
+     apply (le_plus_to_le a).
+     assumption
+    ]
+  ]
+qed.
+
+theorem le_exp_to_le: 
+\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
+intro.
+apply nat_elim2;intros
+  [apply le_O_n
+  |apply False_ind.
+   apply (le_to_not_lt ? ? H1).
+   simplify.
+   rewrite > times_n_SO.
+   apply lt_to_le_to_lt_times
+    [assumption
+    |apply lt_O_exp.apply lt_to_le.assumption
+    |apply lt_O_exp.apply lt_to_le.assumption
+    ]
+  |simplify in H2.
+   apply le_S_S.
+   apply H
+    [assumption
+    |apply (le_times_to_le a)
+      [apply lt_to_le.assumption|assumption]
+    ]
+  ]
+qed.
+
+theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. 
+O < n \to O < m \to prime p 
+\to divides n m \to p_ord n p = pair ? ? a b \to
+p_ord m p = pair ? ? c d \to divides b d \land a \le c.
+intros.
+cut (S O < p)
+  [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
+   lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
+   elim Hletin. clear Hletin.
+   elim Hletin1. clear Hletin1.
+   rewrite > H9 in H3.
+   split
+    [apply (gcd_SO_to_divides_times_to_divides (exp p c))
+      [elim (le_to_or_lt_eq ? ? (le_O_n b))
+        [assumption
+        |apply False_ind.
+         apply (lt_to_not_eq O ? H).
+         rewrite > H7.
+         rewrite < H10.
+         auto
+        ]
+      |elim c
+        [rewrite > sym_gcd.
+         apply gcd_SO_n
+        |simplify.
+         apply eq_gcd_times_SO
+          [apply lt_to_le.assumption
+          |apply lt_O_exp.apply lt_to_le.assumption
+          |rewrite > sym_gcd.
+           (* hint non trova prime_to_gcd_SO e
+              auto non chiude il goal *)
+           apply prime_to_gcd_SO
+            [assumption|assumption]
+          |assumption
+          ]
+        ]
+      |apply (trans_divides ? n)
+        [apply (witness ? ? (exp p a)).
+         rewrite > sym_times.
+         assumption
+        |assumption
+        ]
+      ]
+    |apply (le_exp_to_le p)
+      [assumption
+      |apply divides_to_le
+        [apply lt_O_exp.apply lt_to_le.assumption
+        |apply (gcd_SO_to_divides_times_to_divides d)
+          [apply lt_O_exp.apply lt_to_le.assumption
+          |elim a
+            [apply gcd_SO_n
+            |simplify.rewrite < sym_gcd.
+             apply eq_gcd_times_SO
+              [apply lt_to_le.assumption
+              |apply lt_O_exp.apply lt_to_le.assumption
+              |rewrite > sym_gcd.
+              (* hint non trova prime_to_gcd_SO e
+                 auto non chiude il goal *)
+               apply prime_to_gcd_SO
+                [assumption|assumption]
+              |rewrite > sym_gcd. assumption
+              ]
+            ]
+          |apply (trans_divides ? n)
+            [apply (witness ? ? b).assumption
+            |rewrite > sym_times.assumption
+            ]
+          ]
+        ]
+      ]
+    ]
+  |elim H2.assumption
+  ]
+qed.     
+
+definition ord :nat \to nat \to nat \def
+\lambda n,p. fst ? ? (p_ord n p).
+
+definition ord_rem :nat \to nat \to nat \def
+\lambda n,p. snd ? ? (p_ord n p).
+         
+theorem divides_to_ord: \forall p,n,m:nat. 
+O < n \to O < m \to prime p 
+\to divides n m 
+\to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).  
+intros.
+apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
+  [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+  |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+  ]
+qed.
+
+theorem divides_to_divides_ord_rem: \forall p,n,m:nat. 
+O < n \to O < m \to prime p \to divides n m \to
+divides (ord_rem n p) (ord_rem m p).
+intros.
+elim (divides_to_ord p n m H H1 H2 H3).assumption.
+qed.
+
+theorem divides_to_le_ord: \forall p,n,m:nat. 
+O < n \to O < m \to prime p \to divides n m \to
+(ord n p) \le (ord m p).  
+intros.
+elim (divides_to_ord p n m H H1 H2 H3).assumption.
+qed.
+
+theorem exp_ord: \forall p,n. (S O) \lt p 
+\to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
+intros.
+elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
+  [assumption
+  |assumption
+  |assumption
+  |unfold ord.unfold ord_rem.
+   apply eq_pair_fst_snd
+  ]
+qed.
+
+theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n 
+\to divides (ord_rem n p) n. 
+intros.
+apply (witness ? ? (p \sup (ord n p))).
+rewrite > sym_times. 
+apply exp_ord[assumption|assumption]
+qed.
+
+theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p. 
+intros.
+elim (le_to_or_lt_eq O (ord_rem n p))
+  [assumption
+  |apply False_ind.
+   apply (lt_to_not_eq ? ? H1).
+   lapply (divides_ord_rem ? ? H H1).
+   rewrite < H2 in Hletin.
+   elim Hletin.
+   rewrite > H3.
+   reflexivity
+  |apply le_O_n
+  ]
+qed.
diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 8c6ce942e..8be62ae0b 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -201,7 +201,7 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
-(* le to eq *)
+(* le and eq *)
 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
 apply nat_elim2
   [intros.apply le_n_O_to_eq.assumption
diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index c5fe7bd29..4298eb942 100644
--- a/matita/library/nat/primes.ma
+++ b/matita/library/nat/primes.ma
@@ -193,7 +193,7 @@ qed.
 (* boolean divides *)
 definition divides_b : nat \to nat \to bool \def
 \lambda n,m :nat. (eqb (m \mod n) O).
-  
+
 theorem divides_b_to_Prop :
 \forall n,m:nat. O < n \to
 match divides_b n m with
@@ -205,7 +205,7 @@ intro.simplify.apply mod_O_to_divides.assumption.assumption.
 intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 qed.
 
-theorem divides_b_true_to_divides :
+theorem divides_b_true_to_divides1:
 \forall n,m:nat. O < n \to
 (divides_b n m = true ) \to n \divides m.
 intros.
@@ -217,7 +217,21 @@ rewrite < H1.apply divides_b_to_Prop.
 assumption.
 qed.
 
-theorem divides_b_false_to_not_divides :
+theorem divides_b_true_to_divides:
+\forall n,m:nat. divides_b n m = true \to n \divides m.
+intros 2.apply (nat_case n)
+  [apply (nat_case m)
+    [intro.apply divides_n_n
+    |simplify.intros.apply False_ind.
+     apply not_eq_true_false.apply sym_eq.assumption
+    ]
+  |intros.
+   apply divides_b_true_to_divides1
+    [apply lt_O_S|assumption]
+  ]
+qed.
+
+theorem divides_b_false_to_not_divides1:
 \forall n,m:nat. O < n \to
 (divides_b n m = false ) \to n \ndivides m.
 intros.
@@ -229,6 +243,22 @@ rewrite < H1.apply divides_b_to_Prop.
 assumption.
 qed.
 
+theorem divides_b_false_to_not_divides:
+\forall n,m:nat. divides_b n m = false \to n \ndivides m.
+intros 2.apply (nat_case n)
+  [apply (nat_case m)
+    [simplify.unfold Not.intros.
+     apply not_eq_true_false.assumption
+    |unfold Not.intros.elim H1.
+     apply (not_eq_O_S m1).apply sym_eq.
+     assumption
+    ]
+  |intros.
+   apply divides_b_false_to_not_divides1
+    [apply lt_O_S|assumption]
+  ]
+qed.
+
 theorem decidable_divides: \forall n,m:nat.O < n \to
 decidable (n \divides m).
 intros.unfold decidable.
@@ -263,6 +293,21 @@ absurd (n \divides m).assumption.assumption.
 reflexivity.
 qed.
 
+theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n m))
+  [assumption
+  |apply False_ind.
+   elim H1.
+   rewrite < H2 in H1.
+   simplify in H1.
+   apply (lt_to_not_eq O n H).
+   apply sym_eq.
+   apply eqb_true_to_eq.
+   assumption
+  ]
+qed.
+
 (* divides and pi *)
 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. 
 m \le i \to i \le n+m \to f i \divides pi n f m.
@@ -323,10 +368,8 @@ theorem not_divides_S_fact: \forall n,i:nat.
 (S O) < i \to i \le n \to i \ndivides S n!.
 intros.
 apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
 unfold divides_b.
-rewrite > mod_S_fact.simplify.reflexivity.
-assumption.assumption.
+rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption].
 qed.
 
 (* prime *)
@@ -401,7 +444,6 @@ intro.apply (nat_case m).intro. simplify.
 apply (witness ? ? (S O)). simplify.reflexivity.
 intros.
 apply divides_b_true_to_divides.
-apply (lt_O_smallest_factor ? H).
 change with 
 (eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) 
   (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
@@ -431,7 +473,6 @@ apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
 intros.
 apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b.
 apply (lt_min_aux_to_false 
 (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i).
 cut ((S(S O)) = (S(S m1)-m1)).