fact: Definition miller_rabin (l : list Z) (n : Z) : bool := if n <? 2 then false else if n =? 2 then true else Z.odd n && let (s, d) := remove_twos (Z.to_pos (n - 1)) in forallb (fun a => implb ((0 <? a) && (a <? n)) ((pow_mod n a (Zpos d) =? 1) || existsb (fun r => pow_mod n a (2 ^ r * Zpos d) =? n - 1) (Zseq 0 s))) l.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)