fact: Fixpoint remove_twos (x : positive) : (nat * positive) := match x with | xO p => let (k, d) := remove_twos p in (S k, d) | _ => (O, x) end.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)