proposition: Lemma MR_range_spec_0 l b : MR_range l 0 b = true -> forall n : Z, n <= b -> miller_rabin l n = primeb n.
proof: Proof. intros h n nb. pose proof proj1 (MR_range_spec _ _ _) h n as m. destruct (n <? 2) eqn:n2. - unfold miller_rabin in *. rewrite n2 in *. destruct (primeb n) eqn:pn; auto. apply Z.ltb_lt in n2. apply primeb_prime, prime_ge_2 in pn. lia. - apply Z.ltb_ge in n2. apply m. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)