proposition: Lemma miller_rabin_2 n : n <= 2046 -> miller_rabin [2] n = primeb n.
proof: Proof. apply MR_range_spec_2. vm_compute. reflexivity. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)