n < smallest_factor (S n!).
intros.
apply not_le_to_lt.
-change with smallest_factor (S n!) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S 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.
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 (S n1)!)).
+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 (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 (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.
theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
intro.
-apply nat_case n.
-change with prime (S(S O)).
-apply primeb_to_Prop (S(S O)).
+apply (nat_case n).
+change with (prime (S(S O))).
+apply (primeb_to_Prop (S(S O))).
intro.
change with
-let previous_prime \def (nth_prime m) in
+(let previous_prime \def (nth_prime m) in
let upper_bound \def S previous_prime! in
-prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
+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 (nth_prime m)!)).
+apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
split.split.
-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).
+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 plus_minus_m_m.
apply le_smallest_factor_n.
apply prime_to_primeb_true.
apply prime_smallest_factor_n.
-change with (S(S O)) \le S (nth_prime m)!.
+change with ((S(S O)) \le S (nth_prime m)!).
apply le_S_S.apply le_SO_fact.
qed.
(* properties of nth_prime *)
theorem increasing_nth_prime: increasing nth_prime.
-change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
+change with (\forall n:nat. (nth_prime n) < (nth_prime (S n))).
intros.
change with
-let previous_prime \def (nth_prime n) in
+(let previous_prime \def (nth_prime n) in
let upper_bound \def S previous_prime! in
-(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
+(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).
+cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime)).
rewrite < Hcut in \vdash (? % ?).
apply le_min_aux.
apply plus_to_minus.
theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
intros. elim n.simplify.apply le_n.
-apply trans_lt ? (nth_prime n1).
+apply (trans_lt ? (nth_prime n1)).
assumption.apply lt_nth_prime_n_nth_prime_Sn.
qed.
theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
-intros.apply trans_lt O (S O).
+intros.apply (trans_lt O (S O)).
simplify. apply le_n.apply lt_SO_nth_prime_n.
qed.
\to \lnot (prime m).
intros.
apply primeb_false_to_not_prime.
-letin previous_prime \def nth_prime n.
-letin upper_bound \def S previous_prime!.
-apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
-cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
+letin previous_prime \def (nth_prime n).
+letin upper_bound \def (S previous_prime!).
+apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m).
+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 plus_minus_m_m.
theorem prime_to_nth_prime : \forall p:nat. prime p \to
\exists i. nth_prime i = p.
intros.
-cut \exists m. nth_prime m \le p \land p < nth_prime (S m).
+cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
elim Hcut.elim H1.
-cut nth_prime a < p \lor nth_prime a = p.
+cut (nth_prime a < p \lor nth_prime a = p).
elim Hcut1.
absurd (prime p).
assumption.
-apply lt_nth_prime_to_not_prime a.assumption.assumption.
-apply ex_intro nat ? a.assumption.
+apply (lt_nth_prime_to_not_prime a).assumption.assumption.
+apply (ex_intro nat ? a).assumption.
apply le_to_or_lt_eq.assumption.
apply ex_m_le_n_nth_prime_m.
simplify.simplify in H.elim H.assumption.