X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=6913562439f6e0f45d195241fa7fcecd8d3bc353;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=be3660187d7d1b126c7c35adf04554fa09b65ea4;hpb=63e834c4fbcb3d015f418989ccd6d2fc8c3dd9ab;p=helm.git

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index be3660187..691356243 100644
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -72,6 +72,10 @@ theorem divides_n_O: \forall n:nat. n \divides O.
 intro. apply witness n O O.apply times_n_O.
 qed.
 
+theorem divides_n_n: \forall n:nat. n \divides n.
+intro. apply witness n n (S O).apply times_n_SO.
+qed.
+
 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
 intro. apply witness (S O) n n. simplify.apply plus_n_O.
 qed.
@@ -116,6 +120,36 @@ qed.
 variant trans_divides: \forall n,m,p. 
  n \divides m \to m \divides p \to n \divides p \def transitive_divides.
 
+theorem eq_mod_to_divides:\forall n,m,p. O< p \to
+mod n p = mod m p \to divides p (n-m).
+intros.
+cut n \le m \or \not n \le m.
+elim Hcut.
+cut n-m=O.
+rewrite > Hcut1.
+apply witness p O O.
+apply times_n_O.
+apply eq_minus_n_m_O.
+assumption.
+apply witness p (n-m) ((div n p)-(div m p)).
+rewrite > distr_times_minus.
+rewrite > sym_times.
+rewrite > sym_times p.
+cut (div n p)*p = n - (mod n p).
+rewrite > Hcut1.
+rewrite > eq_minus_minus_minus_plus.
+rewrite > sym_plus.
+rewrite > H1.
+rewrite < div_mod.reflexivity.
+assumption.
+apply sym_eq.
+apply plus_to_minus.
+rewrite > sym_plus.
+apply div_mod.
+assumption.
+apply decidable_le n m.
+qed.
+
 (* divides le *)
 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
 intros. elim H1.rewrite > H2.cut O < n2.
@@ -217,21 +251,23 @@ reflexivity.
 qed.
 
 (* divides and pi *)
-theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat. 
-i < n \to f i \divides pi n f.
-intros 3.elim n.apply False_ind.apply not_le_Sn_O i H.
+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.
+intros 5.elim n.simplify.
+cut i = m.rewrite < Hcut.apply divides_n_n.
+apply antisymmetric_le.assumption.assumption.
 simplify.
-apply le_n_Sm_elim (S i) n1 H1.
-intro.
-apply transitive_divides ? (pi n1 f).
-apply H.simplify.apply le_S_S_to_le. assumption.
-apply witness ? ? (f n1).apply sym_times.
-intro.cut i = n1.
-rewrite > Hcut.
-apply witness ? ? (pi n1 f).reflexivity.
-apply inj_S.assumption.
+cut i < S n1+m \lor i = S n1 + m.
+elim Hcut.
+apply transitive_divides ? (pi n1 f m).
+apply H1.apply le_S_S_to_le. assumption.
+apply witness ? ? (f (S n1+m)).apply sym_times.
+rewrite > H3.
+apply witness ? ? (pi n1 f m).reflexivity.
+apply le_to_or_lt_eq.assumption.
 qed.
 
+(*
 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. 
 i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
 intros.cut (pi n f) \mod (f i) = O.
@@ -241,6 +277,7 @@ rewrite > Hcut.assumption.
 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
 apply divides_f_pi_f.assumption.
 qed.
+*)
 
 (* divides and fact *)
 theorem divides_fact : \forall n,i:nat. 
@@ -328,7 +365,7 @@ apply le_n (S(S O)).
 cut (S(S O)) = (S(S m1)) - m1.
 rewrite > Hcut.
 apply le_min_aux.
-apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn.
+apply sym_eq.apply plus_to_minus.
 rewrite < sym_plus.simplify.reflexivity.
 qed.
 
@@ -388,7 +425,6 @@ apply lt_min_aux_to_false
 cut (S(S O)) = (S(S m1)-m1).
 rewrite < Hcut.exact H1.
 apply sym_eq. apply plus_to_minus.
-apply le_S.apply le_n_Sn.
 rewrite < sym_plus.simplify.reflexivity.
 exact H2.
 qed.