(* divides and fact *)
theorem divides_fact : \forall n,i:nat.
-O < i \to i \le n \to divides i (fact n).
+O < i \to i \le n \to divides i (n !).
intros 3.elim n.absurd O<i.assumption.apply le_n_O_elim i H1.
apply not_le_Sn_O O.
-change with divides i ((S n1)*(fact n1)).
+change with divides i ((S n1)*(n1 !)).
apply le_n_Sm_elim i n1 H2.
intro.
-apply transitive_divides ? (fact n1).
+apply transitive_divides ? (n1 !).
apply H1.apply le_S_S_to_le. assumption.
apply witness ? ? (S n1).apply sym_times.
intro.
rewrite > H3.
-apply witness ? ? (fact n1).reflexivity.
+apply witness ? ? (n1 !).reflexivity.
qed.
theorem mod_S_fact: \forall n,i:nat.
-(S O) < i \to i \le n \to mod (S (fact n)) i = (S O).
-intros.cut mod (fact n) i = O.
+(S O) < i \to i \le n \to mod (S (n !)) i = (S O).
+intros.cut mod (n !) i = O.
rewrite < Hcut.
apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
rewrite > Hcut.assumption.
qed.
theorem not_divides_S_fact: \forall n,i:nat.
-(S O) < i \to i \le n \to \not (divides i (S (fact n))).
+(S O) < i \to i \le n \to \not (divides i (S (n !))).
intros.
apply divides_b_false_to_not_divides.
apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb (mod (S (fact n)) i) O) = false.
+change with (eqb (mod (S (n !)) i) O) = false.
rewrite > mod_S_fact.simplify.reflexivity.
assumption.assumption.
qed.