More notation here and there.

[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 dc5f627e43103119199d71747a837c60b8595cf4..505d3de496053c56b8de48232387891ea19a5a1e 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -237,23 +237,23 @@ qed.
 
 (* 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.
@@ -263,11 +263,11 @@ 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.