+include "nat/congruence.ma".
+
+theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
+intro.unfold permut.split.intros.
+unfold S_mod.
+apply le_S_S_to_le.
+change with ((S i) \mod (S n) < S n).
+apply lt_mod_m_m.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold injn.intros.
+apply inj_S.
+rewrite < (lt_to_eq_mod i (S n)).
+rewrite < (lt_to_eq_mod j (S n)).
+cut (i < n \lor i = n).
+cut (j < n \lor j = n).
+elim Hcut.
+elim Hcut1.
+(* i < n, j< n *)
+rewrite < mod_S.
+rewrite < mod_S.
+apply H2.unfold lt.apply le_S_S.apply le_O_n.
+rewrite > lt_to_eq_mod.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite > lt_to_eq_mod.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+(* i < n, j=n *)
+unfold S_mod in H2.
+simplify.
+apply False_ind.
+apply (not_eq_O_S (i \mod (S n))).
+apply sym_eq.
+rewrite < (mod_n_n (S n)).
+rewrite < H4 in \vdash (? ? ? (? %?)).
+rewrite < mod_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite > lt_to_eq_mod.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+(* i = n, j < n *)
+elim Hcut1.
+apply False_ind.
+apply (not_eq_O_S (j \mod (S n))).
+rewrite < (mod_n_n (S n)).
+rewrite < H3 in \vdash (? ? (? %?) ?).
+rewrite < mod_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite > lt_to_eq_mod.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+(* i = n, j= n*)
+rewrite > H3.
+rewrite > H4.
+reflexivity.
+apply le_to_or_lt_eq.assumption.
+apply le_to_or_lt_eq.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+qed.
+
+(*
+theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
+intro.elim n.
+simplify.reflexivity.
+change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
+unfold S_mod in \vdash (? ? ? (? % ?)).
+rewrite > lt_to_eq_mod.
+apply eq_f.apply H.apply (trans_lt ? (S n1)).
+simplify. apply le_n.assumption.assumption.
+qed.
+*)
+
+theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
+n \lt p \to \not divides p n!.
+intros 3.elim n.unfold Not.intros.
+apply (lt_to_not_le (S O) p).
+unfold prime in H.elim H.
+assumption.apply divides_to_le.unfold lt.apply le_n.
+assumption.
+change with (divides p ((S n1)*n1!) \to False).
+intro.
+cut (divides p (S n1) \lor divides p n1!).
+elim Hcut.apply (lt_to_not_le (S n1) p).
+assumption.
+apply divides_to_le.unfold lt.apply le_S_S.apply le_O_n.
+assumption.apply H1.
+apply (trans_lt ? (S n1)).unfold lt. apply le_n.
+assumption.assumption.
+apply divides_times_to_divides.
+assumption.assumption.
+qed.