proposition: Theorem bad_get_primediv_ok : forall n:nat, 1 < n -> prime_divisor n (bad_get_prime n).
proof: Proof. intros n H; unfold bad_get_prime. Abort. Definition stronger_prime_test : forall n:nat, {(prime_test n)=true}+{(prime_test n)=false}. Proof. intro n; case (prime_test n);[left | right]; reflexivity. Defined.
imports: ZArith List Arith Lia Zwf