proposition: Lemma MR_range_empty l a b : a > b -> MR_range l a b = true.
proof: Proof. intros ab. unfold MR_range. replace (Z.to_nat _) with O by lia. easy. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)