proposition: Lemma miller_rabin_2_3 n : n <= 10000 -> miller_rabin [2; 3] n = primeb n.
proof: Proof. apply MR_range_spec_2. Time vm_compute. reflexivity. Time Qed. Lemma first_miller_rabin_2_3_pseudo_prime : miller_rabin [2; 3] 1373653 = true /\ miller_rabin [2; 3; 5] 1373653 = false /\ primeb 1373653 = false. Proof. now vm_compute. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)