X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;h=84407538d2a89236188a3f5dab7e5f111f13338a;hb=5c6b8eec9db4119a87eb4fd4055f1ac31a713d90;hp=200ccba5a9086b0ca2a940c7f19ae0964bb8402c;hpb=ab44166935d77276c04fcce50aa8281292776e29;p=helm.git

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 200ccba5a..84407538d 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -39,11 +39,11 @@ normalize.reflexivity.
 qed. *)
 
 theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (fact n)).
+n < smallest_factor (S n!).
 intros.
 apply not_le_to_lt.
-change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))).
+change with smallest_factor (S n!) \le n \to False.intro.
+apply not_divides_S_fact n (smallest_factor(S n!)).
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.
@@ -52,19 +52,19 @@ simplify.apply le_S_S.apply le_O_n.
 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
-n < m \land m \le (S (fact n)) \land (prime m).
+n < m \land m \le S n! \land (prime m).
 intros.
 elim H.
 apply ex_intro nat ? (S(S O)).
 split.split.apply le_n (S(S O)).
 apply le_n (S(S O)).apply primeb_to_Prop (S(S O)).
-apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
+apply ex_intro nat ? (smallest_factor (S (S n1)!)).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
 (* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (S n1)).
+change with (S(S O)) \le S (S n1)!.
 apply le_S.apply le_SSO_fact.
 simplify.apply le_S_S.assumption.
 qed.
@@ -74,7 +74,7 @@ match n with
   [ O \Rightarrow (S(S O))
   | (S p) \Rightarrow
     let previous_prime \def (nth_prime p) in
-    let upper_bound \def S (fact previous_prime) in
+    let upper_bound \def S previous_prime! in
     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
     
 (* it works, but nth_prime 4 takes already a few minutes -
@@ -100,24 +100,23 @@ apply primeb_to_Prop (S(S O)).
 intro.
 change with
 let previous_prime \def (nth_prime m) in
-let upper_bound \def S (fact previous_prime) in
+let upper_bound \def S previous_prime! in
 prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
 apply primeb_true_to_prime.
 apply f_min_aux_true.
-apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))).
+apply ex_intro nat ? (smallest_factor (S (nth_prime m)!)).
 split.split.
-cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)).
+cut S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m)).
 rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
 (* maybe we could factorize this proof *)
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.
 apply le_smallest_factor_n.
 apply prime_to_primeb_true.
 apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (nth_prime m)).
+change with (S(S O)) \le S (nth_prime m)!.
 apply le_S_S.apply le_SO_fact.
 qed.
 
@@ -127,14 +126,13 @@ change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
 intros.
 change with
 let previous_prime \def (nth_prime n) in
-let upper_bound \def S (fact previous_prime) in
+let upper_bound \def S previous_prime! in
 (S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
 intros.
 cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
 rewrite < Hcut in \vdash (? % ?).
 apply le_min_aux.
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.
@@ -168,16 +166,15 @@ exact lt_nth_prime_n_nth_prime_Sn.assumption.
 qed.
 
 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) 
-\to \not (prime m).
+\to \lnot (prime m).
 intros.
 apply primeb_false_to_not_prime.
 letin previous_prime \def nth_prime n.
-letin upper_bound \def S (fact previous_prime).
+letin upper_bound \def S previous_prime!.
 apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
-cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)).
+cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
 rewrite > Hcut.assumption.
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.