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

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

diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma
index 470bb9d69f7ea3992ff413b7f63ad7ff3879228f..6bd6af38c52eae0f4163938fd245f3bfa4e1b657 100644 (file)
--- a/helm/matita/library/nat/sigma_and_pi.ma
+++ b/helm/matita/library/nat/sigma_and_pi.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/sigma_and_pi".
 
+include "nat/factorial.ma".
 include "nat/lt_arith.ma".
 
 let rec sigma n f \def
@@ -47,3 +48,10 @@ apply eq_f2.apply H1.simplify. apply le_n.
 apply H.intros.apply H1.
 apply trans_lt ? n1.assumption.simplify.apply le_n.
 qed.
+
+theorem eq_fact_pi: \forall n. n! = pi n S.
+intro.elim n.
+simplify.reflexivity.
+change with (S n1)*n1! = (S n1)*(pi n1 S).
+apply eq_f.assumption.
+qed.
\ No newline at end of file