fact: Fixpoint mainloop n s x := match s with | O => false | S s => (x =? n - 1) || mainloop n s ((x * x) mod n) end.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)