proposition: Lemma MR_range_spec l a b : MR_range l a b = true <-> (forall n : Z, a <= n <= b -> miller_rabin l n = primeb n).
proof: Proof. unfold MR_range. rewrite forallb_forall. apply iff_intro; intros x. apply iff_intro_Prop. rewrite in_Zseq; lia. intros _ bx. unfold MR_at in *. destruct (miller_rabin l x) eqn:e. split; auto. destruct (primeb x) eqn:p; split; auto. apply miller_rabin_sound in e. now apply primeb_prime in p. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)