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.
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.
[ 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 -
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_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.
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).
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.