]> matita.cs.unibo.it Git - helm.git/commitdiff
New contrib moebius.ma.
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 16 Mar 2007 08:05:44 +0000 (08:05 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 16 Mar 2007 08:05:44 +0000 (08:05 +0000)
helm/software/matita/library/Z/moebius.ma [new file with mode: 0644]
helm/software/matita/library/Z/sigma_p.ma [new file with mode: 0644]

diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma
new file mode 100644 (file)
index 0000000..e91bf8d
--- /dev/null
@@ -0,0 +1,529 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/Z/moebius".
+
+include "nat/factorization.ma".
+include "Z/sigma_p.ma".
+  
+let rec moebius_aux p n : Z \def
+  match p with 
+  [ O \Rightarrow pos O
+  | (S p1) \Rightarrow 
+    match p_ord n (nth_prime p1) with
+    [ (pair q r) \Rightarrow
+      match q with
+      [ O \Rightarrow moebius_aux p1 r
+      | (S q1) \Rightarrow
+             match q1 with 
+             [ O \Rightarrow Zopp (moebius_aux p1 r) 
+        | (S q2) \Rightarrow OZ
+        ]
+      ]
+    ]
+  ]
+.
+
+definition moebius : nat \to Z \def
+\lambda n.
+  let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
+  moebius_aux (S p) n.
+
+theorem moebius_O : moebius O = pos O.
+simplify. reflexivity.
+qed.
+      
+theorem moebius_SO : moebius (S O) = pos O.
+simplify.reflexivity.
+qed.  
+
+theorem moebius_SSO : moebius (S (S O)) = neg O.
+simplify.reflexivity.
+qed.  
+
+theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
+simplify.reflexivity.
+qed.
+
+
+theorem not_divides_to_p_ord_O: \forall n,i.
+Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = 
+pair nat nat O n.
+intros.
+apply p_ord_exp1
+  [apply lt_O_nth_prime_n
+  |assumption
+  |auto
+  ]
+qed.
+
+theorem p_ord_O_to_not_divides: \forall n,i,r.
+O < n \to
+p_ord n (nth_prime i) = pair nat nat O r 
+\to Not (divides (nth_prime i) n).
+intros.
+lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+  [apply lt_SO_nth_prime_n
+  |assumption
+  |elim Hletin.
+   simplify in H3.
+   rewrite > H3.
+   rewrite < plus_n_O.
+   assumption
+  ]
+qed.
+
+theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
+(\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
+\to moebius_aux p n = moebius_aux p1 n.
+intros 4.
+elim H
+  [reflexivity
+  |simplify.
+   rewrite > not_divides_to_p_ord_O
+    [simplify.apply H2.intros.
+     apply H3[assumption|apply le_S.assumption]
+    |apply H3[assumption|apply le_n_Sn]
+    ]
+  ]
+qed.
+
+theorem eq_moebius_moebius_aux: \forall n,p. 
+max_prime_factor n < p \to p \le n \to
+moebius n = moebius_aux p n.
+intros.
+unfold moebius.
+change with 
+(moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
+= moebius_aux p n).
+apply not_divides_to_eq_moebius_aux
+  [assumption
+  |intros.
+   apply divides_b_false_to_not_divides.
+   unfold divides_b.
+   apply (lt_max_to_false ? n i)
+    [assumption
+    |apply (trans_le ? p)[assumption|assumption]
+    ]
+  ]
+qed.
+
+theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
+intros.
+elim p
+  [simplify.reflexivity
+  |rewrite < H.
+   apply sym_eq.
+   apply not_divides_to_eq_moebius_aux
+   [apply le_n_Sn
+   |intros.unfold.intro.
+    absurd (nth_prime i \le S O)
+      [apply divides_to_le
+        [apply le_n|assumption]
+      |apply lt_to_not_le.
+       apply lt_SO_nth_prime_n.
+      ]
+    ]
+  ]
+qed.
+
+theorem p_ord_to_not_eq_O : \forall n,p,q,r.
+  (S O) < n \to
+  p_ord n (nth_prime p) = pair nat nat q r \to
+  Not (r=O).
+intros.
+unfold.intro.
+cut (O < n)
+  [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+    [apply lt_SO_nth_prime_n.
+    |assumption
+    |elim Hletin.
+     apply (lt_to_not_eq ? ? Hcut).
+     rewrite > H4.
+     rewrite > H2.
+     apply times_n_O
+    ]
+  |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+  ]
+qed.
+
+theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
+  (S O) < n \to
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) \neq pair nat nat O r.
+intros.unfold Not.intro.
+apply (p_ord_O_to_not_divides ? ? ? ? H2)
+  [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+  |rewrite > H1.
+   apply divides_max_prime_factor_n.
+   assumption
+  ]
+qed.
+
+theorem p_ord_SO_SO_to_moebius : \forall n,p.
+  (S O) < n \to
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
+  moebius n = Zopp (pos O).
+intros.
+change with 
+  (moebius_aux (S (max_prime_factor n)) n = neg O).
+rewrite < H1.simplify.
+rewrite > H2.simplify.
+rewrite > moebius_aux_SO.
+reflexivity.
+qed.
+
+theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
+  (S O) < n \to 
+  p = max_prime_factor n \to
+  (S O) < r \to 
+  p_ord n (nth_prime p) = pair nat nat (S O) r \to
+  moebius n = Zopp (moebius r).
+intros.
+change with 
+  (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
+rewrite < H1.simplify.
+rewrite > H3.simplify.
+apply eq_f.
+apply sym_eq.
+change with 
+ (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
+apply not_divides_to_eq_moebius_aux
+  [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
+    [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+    |apply sym_eq. assumption
+    |assumption
+    ]
+  |intros.
+   lapply (decidable_le i r).
+   elim Hletin
+    [apply divides_b_false_to_not_divides.
+     apply (lt_max_to_false ? r i)[assumption|assumption]
+    |unfold.intro.apply H6.
+     apply (trans_le ? (nth_prime i))
+      [apply lt_to_le.
+       apply lt_n_nth_prime_n
+      |apply divides_to_le
+        [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
+theorem p_ord_SO_r_to_moebius : \forall n,p,r.
+  (S O) < n \to 
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) = pair nat nat (S O) r \to
+  moebius n = Zopp (moebius r).
+intros 5.
+apply (nat_case r);intro
+  [apply False_ind.
+   apply (p_ord_to_not_eq_O ? ? ? ? H H2).
+   reflexivity
+  |apply (nat_case m);intros
+    [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
+    |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
+     apply le_S_S.apply le_S_S.apply le_O_n
+    ]
+  ]
+qed.    
+
+theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
+  (S O) < n \to
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
+  moebius n = OZ.
+intros.
+change with
+  (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
+rewrite < H1.simplify.
+rewrite > H2.simplify.
+reflexivity.
+qed.
+
+lemma eq_p_max: \forall n,p,r:nat. O < n \to
+O < r \to
+r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
+p = max_prime_factor (r*(nth_prime p)\sup n).
+intros.
+apply sym_eq.
+unfold max_prime_factor.
+apply max_spec_to_max.
+split
+  [split
+    [rewrite > times_n_SO in \vdash (? % ?).
+     rewrite > sym_times.
+     apply le_times
+      [assumption
+      |apply lt_to_le.
+       apply (lt_to_le_to_lt ? (nth_prime p))
+        [apply lt_n_nth_prime_n
+        |rewrite > exp_n_SO in \vdash (? % ?).
+         apply le_exp
+          [apply lt_O_nth_prime_n
+          |assumption
+          ]
+        ]
+      ]
+    |apply eq_to_eqb_true.
+     apply divides_to_mod_O
+      [apply lt_O_nth_prime_n
+      |apply (lt_O_n_elim ? H).
+       intro.
+       apply (witness ? ? (r*(nth_prime p \sup m))).
+       rewrite < assoc_times.
+       rewrite < sym_times in \vdash (? ? ? (? % ?)).
+       rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
+       rewrite > assoc_times.
+       rewrite < exp_plus_times.
+       reflexivity
+      ]
+    ]
+  |intros.  
+   apply not_eq_to_eqb_false.
+   unfold Not.intro.
+   lapply (mod_O_to_divides ? ? ? H5)
+    [apply lt_O_nth_prime_n
+    |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
+      [elim H2
+        [rewrite > H6 in Hletin.
+         simplify in Hletin.
+         rewrite < plus_n_O in Hletin.
+         apply Hcut.assumption
+        |elim (divides_times_to_divides ? ? ? ? Hletin)
+          [apply (lt_to_not_le ? ? H3).
+           apply lt_to_le. 
+           apply (le_to_lt_to_lt ? ? ? ? H6).
+           apply f_m_to_le_max
+            [apply (trans_le ? (nth_prime i))
+              [apply lt_to_le.
+               apply lt_n_nth_prime_n
+              |apply divides_to_le[assumption|assumption]
+              ]
+            |apply eq_to_eqb_true.
+             apply divides_to_mod_O
+              [apply lt_O_nth_prime_n|assumption]
+            ]
+          |apply prime_nth_prime
+          |apply Hcut.assumption
+          ]
+        ]
+      |unfold Not.intro.
+       apply (lt_to_not_eq ? ? H3).
+       apply sym_eq.
+       elim (prime_nth_prime p).
+       apply injective_nth_prime.
+       apply H8
+        [apply (divides_exp_to_divides ? ? ? ? H6).
+         apply prime_nth_prime.
+        |apply lt_SO_nth_prime_n
+        ]
+      ]
+    ]
+  ]
+qed.
+
+lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
+O < n \to n=S O \lor max_prime_factor n < p \to 
+(nth_prime p \ndivides n).
+intros.unfold Not.intro.
+elim H1
+  [rewrite > H3 in H2.
+   apply (le_to_not_lt (nth_prime p) (S O))
+    [apply divides_to_le[apply le_n|assumption]
+    |apply lt_SO_nth_prime_n
+    ]
+  |apply (not_le_Sn_n p).
+   change with (p < p).
+   apply (le_to_lt_to_lt ? ? ? ? H3).
+   unfold max_prime_factor.
+   apply  f_m_to_le_max
+    [apply (trans_le ? (nth_prime p))
+      [apply lt_to_le.
+       apply lt_n_nth_prime_n
+      |apply divides_to_le;assumption
+      ]
+    |apply eq_to_eqb_true.
+     apply divides_to_mod_O
+      [apply lt_O_nth_prime_n|assumption]
+    ]
+  ]
+qed.
+
+theorem moebius_exp: \forall p,q,r:nat. O < r \to
+r = (S O) \lor (max_prime_factor r) < p \to
+(* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
+sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
+intros.
+elim q
+  [rewrite > true_to_sigma_p_Sn
+    [rewrite > true_to_sigma_p_Sn
+      [rewrite > Zplus_z_OZ.
+       rewrite < times_n_SO.
+       rewrite > (p_ord_SO_r_to_moebius ? p r)
+        [rewrite > sym_Zplus.
+         rewrite > Zplus_Zopp.
+         reflexivity
+        |rewrite < exp_n_SO.
+         rewrite > sym_times.
+         rewrite > times_n_SO.
+         apply lt_to_le_to_lt_times
+          [apply lt_SO_nth_prime_n
+          |assumption
+          |assumption
+          ]
+        |apply eq_p_max
+          [apply le_n|assumption|assumption]
+        |apply p_ord_exp1
+          [apply lt_O_nth_prime_n
+          |apply lt_max_prime_factor_to_not_divides;assumption
+          |apply sym_times
+          ]
+        ]
+      |reflexivity
+      ]
+    |reflexivity
+    ]
+  |rewrite > true_to_sigma_p_Sn
+    [rewrite > H2.
+     rewrite > Zplus_z_OZ.
+     apply (p_ord_SSq_r_to_moebius ? p n r)
+      [rewrite > times_n_SO.
+       rewrite > sym_times in \vdash (? ? %).
+       apply lt_to_le_to_lt_times
+        [apply (trans_lt ? (nth_prime p))
+          [apply lt_SO_nth_prime_n
+            |rewrite > exp_n_SO in \vdash (? % ?).
+             apply lt_exp
+              [apply lt_SO_nth_prime_n
+              |apply le_S_S.apply le_S_S.apply le_O_n
+              ]
+            ]
+          |assumption
+          |assumption
+          ]
+        |apply eq_p_max
+          [apply le_S_S.apply le_O_n|assumption|assumption]  
+        |apply p_ord_exp1
+          [apply lt_O_nth_prime_n
+          |apply lt_max_prime_factor_to_not_divides;assumption        
+          |apply sym_times
+          ]
+        ]
+      |reflexivity
+      ]
+    ]   
+qed.
+  
+theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to 
+n = (S O) \lor max_prime_factor n < p \to
+sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
+intros.
+rewrite > sigma_p_divides_b
+  [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
+    [apply eq_sigma_p1
+      [intros.reflexivity
+      |apply (lt_O_n_elim m H1).
+       intros.apply moebius_exp
+        [apply (divides_b_true_to_lt_O ? ? ? H4).
+         assumption
+        |elim H2
+          [left.rewrite > H5 in H3.
+           elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
+            [apply False_ind.
+             apply (lt_to_not_le O x)
+              [apply (divides_b_true_to_lt_O n x H H4)
+              |apply le_S_S_to_le.assumption
+              ]
+            |assumption
+            ]
+          |right.
+           apply (le_to_lt_to_lt ? ? ? ? H5).
+           apply (divides_to_max_prime_factor1 x n)
+            [apply (divides_b_true_to_lt_O ? ? H H4)
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          ]
+        ]
+      ]
+    |generalize in match (\lambda x:nat.divides_b x n).
+     intro.
+     elim n
+      [simplify.elim (f O);reflexivity
+      |apply (bool_elim ? (f (S n1)))
+        [intro.
+         rewrite > true_to_sigma_p_Sn
+          [rewrite > H3.reflexivity|assumption]
+        |intro.
+         rewrite > false_to_sigma_p_Sn
+          [apply H3|assumption]
+        ]
+      ]
+    ]
+  |assumption
+  |apply prime_nth_prime
+  |apply lt_max_prime_factor_to_not_divides;assumption
+  ]
+qed.
+
+theorem sigma_p_moebius: \forall n. (S O) < n \to
+sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
+intros.
+lapply (exp_ord (nth_prime (max_prime_factor n)) n)
+  [rewrite > sym_times in Hletin.
+   rewrite > Hletin.
+   apply sigma_p_moebius1
+    [apply lt_O_ord_rem
+      [apply lt_SO_nth_prime_n
+      |apply lt_to_le.assumption
+      ]
+    |unfold lt.
+     change with
+      (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
+     rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
+      [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
+        [apply lt_O_nth_prime_n
+        |apply lt_to_le.assumption
+        |apply prime_nth_prime
+        |apply divides_max_prime_factor_n.
+         assumption
+        ]
+      |apply lt_SO_nth_prime_n
+      ]
+    |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
+      [elim (le_to_or_lt_eq ? ? Hletin1)
+        [right.
+         apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n) 
+          (ord n (nth_prime (max_prime_factor n)))
+          (ord_rem n (nth_prime (max_prime_factor n))))
+          [apply lt_to_le.assumption
+          |apply le_n
+          |auto
+          |assumption
+          ]
+        |left.apply sym_eq.assumption
+        ]
+      |apply lt_SO_nth_prime_n
+      |apply lt_to_le.assumption
+      ]
+    ]
+  |apply lt_SO_nth_prime_n
+  |apply lt_to_le.assumption
+  ]
+qed.
diff --git a/helm/software/matita/library/Z/sigma_p.ma b/helm/software/matita/library/Z/sigma_p.ma
new file mode 100644 (file)
index 0000000..27baf8d
--- /dev/null
@@ -0,0 +1,709 @@
+(**************************************************************************)
+(*       ___                                                             *)
+(*      ||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/Z/sigma_p.ma".
+
+include "Z/plus.ma".
+include "nat/primes.ma".
+include "nat/ord.ma".
+
+let rec sigma_p n p (g:nat \to Z) \def
+  match n with
+   [ O \Rightarrow OZ
+   | (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 Z.
+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 Z.
+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 Z.\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 eq_sigma_p1: \forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to Z.\forall n.
+(\forall x.  x < n \to p1 x = p2 x) \to
+(\forall x.  x < n \to p1 x = true \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|assumption]
+        |apply H
+          [intros.apply H1.apply le_S.assumption
+          |intros.apply H2
+            [apply le_S.assumption|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|assumption]
+        ]
+      |rewrite < H3.apply sym_eq.apply H1.apply le_n
+      ]
+    ]
+  ]
+qed.
+
+theorem sigma_p_false: 
+\forall g: nat \to Z.\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 Z.
+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_Zplus.
+     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 Z. (\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 Z.
+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 Z.
+\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_Zplus.
+           rewrite < sym_Zplus in \vdash (? ? ? (? % ?)).
+           rewrite > assoc_Zplus.
+           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: nat \to Z.
+\forall 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 times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
+apply nat_elim2;intros
+  [left.reflexivity
+  |right.reflexivity
+  |apply False_ind.
+   simplify in H1.
+   apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
+  ]
+qed.
+
+theorem prime_to_lt_O: \forall p. prime p \to O < p.
+intros.elim H.apply lt_to_le.assumption.
+qed.
+
+theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
+p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m.
+intros.
+cut (m = ord (n*(exp p m)) p)
+  [apply le_S_S.
+   rewrite > Hcut.
+   apply divides_to_le_ord
+    [elim (le_to_or_lt_eq ? ? (le_O_n j))
+      [assumption
+      |apply False_ind.
+       apply (lt_to_not_eq ? ? H).
+       elim H3.
+       rewrite < H4 in H5.simplify in H5.
+       elim (times_O_to_O ? ? H5)
+        [apply sym_eq.assumption
+        |apply False_ind.
+         apply (not_le_Sn_n O).
+         rewrite < H6 in \vdash (? ? %).
+         apply lt_O_exp.
+         elim H1.apply lt_to_le.assumption
+        ]
+      ]
+    |rewrite > (times_n_O O).
+     apply lt_times
+      [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
+    |assumption
+    |assumption
+    ]
+  |unfold ord.
+   rewrite > (p_ord_exp1 p ? m n)
+    [reflexivity
+    |apply (prime_to_lt_O ? H1)
+    |assumption
+    |apply sym_times
+    ]
+  ]
+qed.
+
+theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to
+p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n.
+intros.
+cut (O < j)
+  [cut (n = ord_rem (n*(exp p m)) p)
+    [rewrite > Hcut1.
+     apply divides_to_divides_ord_rem
+      [assumption   
+      |rewrite > (times_n_O O).
+       apply lt_times
+        [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
+      |assumption
+      |assumption
+      ]
+    |unfold ord_rem.
+     rewrite > (p_ord_exp1 p ? m n)
+      [reflexivity
+      |apply (prime_to_lt_O ? H1)
+      |assumption
+      |apply sym_times
+      ]
+    ]
+  |elim (le_to_or_lt_eq ? ? (le_O_n j))
+    [assumption
+    |apply False_ind.
+     apply (lt_to_not_eq ? ? H).
+     elim H3.
+     rewrite < H4 in H5.simplify in H5.
+     elim (times_O_to_O ? ? H5)
+      [apply sym_eq.assumption
+      |apply False_ind.
+       apply (not_le_Sn_n O).
+       rewrite < H6 in \vdash (? ? %).
+       apply lt_O_exp.
+       elim H1.apply lt_to_le.assumption
+      ]
+    ]
+  ] 
+qed.
+
+theorem sigma_p_divides_b: 
+\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
+\forall g: nat \to Z.
+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]
+              ]
+            |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
+             apply divides_b_true_to_divides.
+             assumption
+            ]
+            |assumption
+          ]
+        |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
+         apply (divides_b_true_to_divides ? ? H4).
+         apply (divides_b_true_to_lt_O ? ? H4)
+        ]
+      |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]
+              ]
+            |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
+             apply (divides_b_true_to_divides ? ? H4).
+             apply (divides_b_true_to_lt_O ? ? H4)
+            ]
+          |assumption
+          ]
+        |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
+         apply (divides_b_true_to_divides ? ? H4).
+         apply (divides_b_true_to_lt_O ? ? H4).
+        ]
+      |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.
+         apply divides_to_le
+          [assumption
+          |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
+           apply divides_b_true_to_divides.
+           assumption
+          ]
+        ]
+      ]
+    |apply eq_sigma_p
+      [intros.
+       elim (divides_b (x/S m) n);reflexivity
+      |intros.reflexivity
+      ]
+    ]
+  |elim H1.apply lt_to_le.assumption
+  ]
+qed.
+