-(* upper bound by Bertrand's conjecture. *)
-(* Too difficult to prove.
-let rec nth_prime n \def
-match n with
- [ O \Rightarrow (S(S O))
- | (S p) \Rightarrow
- let previous_prime \def S (nth_prime p) in
- min_aux previous_prime ((S(S O))*previous_prime) primeb].
-
-theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-normalize.reflexivity.
-qed.
-
-theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-normalize.reflexivity.
-qed.
-
-theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
-normalize.reflexivity.
-qed. *)
-
-theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (fact 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))) ? ?.
-apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_SO_fact.
-apply lt_S_O_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
-assumption.
-qed.
-
-(* mi sembra che il problem sia ex *)
-theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
-n < m \land m \le (S (fact 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)))).
-split.split.
-apply smallest_factor_fact.
-apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
-apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (S n1)).
-apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
-qed.
-
-let rec nth_prime n \def
-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
- 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 ...
-
-theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-normalize.reflexivity.
-qed.
-
-theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-normalize.reflexivity.
-qed.
-
-theorem example13 : nth_prime (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 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
-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)))).
-split.split.
-cut S (fact (nth_prime m))-(S (fact (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)).
-apply le_S_S.apply le_SO_fact.
-qed.
\ No newline at end of file