New entry: fermat's little theorem (almost complete).

[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 be3660187d7d1b126c7c35adf04554fa09b65ea4..1d0fed2967ceb30b3beacac7446c8aa11194efb2 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -116,6 +116,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.
@@ -328,7 +358,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 +418,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.