proposition: Lemma first_miller_rabin_2_pseudo_prime : miller_rabin [2] 2047 = true /\ miller_rabin [2; 3] 2047 = false /\ primeb 2047 = false.
proof: Proof. now vm_compute. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)