fact: Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z := match m with | xH => a mod n | xO m' => let z := Zpow_mod_pos a m' n in match z with | 0 => 0 | _ => (z * z) mod n end | xI m' => let z := Zpow_mod_pos a m' n in match z with | 0 => 0 | _ => (z * z * a) mod n end end.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower