theorem smallest_factor_fact: \forall n:nat.
n < smallest_factor (S n!).
intros.
-apply not_le_to_lt.
-change with (smallest_factor (S n!) \le n \to False).intro.
+apply not_le_to_lt.unfold Not.
+intro.
apply (not_divides_S_fact n (smallest_factor(S n!))).
apply lt_SO_smallest_factor.
unfold lt.apply le_S_S.apply le_SO_fact.
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)!).
+apply prime_smallest_factor_n.unfold lt.
apply le_S.apply le_SSO_fact.
unfold lt.apply le_S_S.assumption.
qed.
min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
(* it works, but nth_prime 4 takes already a few minutes -
-it must compute factorial of 7 ...
+it must compute factorial of 7 ...*)
theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
normalize.reflexivity.
theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
normalize.reflexivity.
+qed.
+
+(*
+theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
*)
theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
intro.
-apply (nat_case n).
-change with (prime (S(S O))).
+apply (nat_case n).simplify.
apply (primeb_to_Prop (S(S O))).
intro.
change with
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 (nth_prime m)!).
+apply prime_smallest_factor_n.unfold lt.
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))).
+unfold increasing.
intros.
change with
(let previous_prime \def (nth_prime n) in