New entry: relevant_equations.

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

diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index aafdc2f19e95a18967eb2b34cea2dc4bce3129e3..5d04a7c816f632dd87eff13a9dc68097de81e95a 100644 (file)
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/fermat_little_theorem".
 
+include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/permutation.ma".
 
@@ -88,3 +89,10 @@ apply trans_lt ? (S O).simplify.apply le_n.assumption.
 apply H4.
 qed.
 
+(*
+theorem bad : \forall p,a:nat. prime p \to \lnot divides p a \to
+mod (exp a (pred p)) p = (S O). 
+intros.
+cut map_iter p (\lambda x.x) times (S O) = 
+map_iter p (\lambda n.(mod (a*n) p)) times (S O).
+*)
\ No newline at end of file