proposition: Theorem prime_fun_sound : forall k, prime_fun k = true -> prime k.
proof: Proof. intros k0; case k0. - simpl; intros; discriminate. - intros k; unfold prime_fun. case_eq (prime_sieve (S k)). + intros; discriminate. + intros (p,n) l Heq; case_eq (Nat.compare p (S k)); try(intros; discriminate; fail). intros Htwc _. assert (Hap:all_first_prime ((p,n)::l)). { generalize (prime_sieve_invariant k ((p,n)::l) Heq); intuition. } rewrite <- (nat_compare_eq _ _ Htwc). apply (Hap nil l p n); auto. Qed.
imports: List Arith