Several changes. Proof of Fermat's little theorem completed.

[helm.git] / helm / matita / library / nat / primes.ma

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 1d0fed2967ceb30b3beacac7446c8aa11194efb2..6913562439f6e0f45d195241fa7fcecd8d3bc353 100644 (file)
--- 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.
@@ -247,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.
@@ -271,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.