More restructuring in moebius.ma

[helm.git] / matita / library / Z / moebius.ma

diff --git a/matita/library/Z/moebius.ma b/matita/library/Z/moebius.ma
index d2c3765c3880b473f3217de64481187fc6a2efb8..1eb35852155109194babd46f20c0992e24516182 100644 (file)
--- a/matita/library/Z/moebius.ma
+++ b/matita/library/Z/moebius.ma
@@ -62,33 +62,6 @@ 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
-  |autobatch
-  ]
-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.
@@ -143,39 +116,6 @@ elim p
   ]
 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
@@ -260,115 +200,6 @@ 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 *)