proposition: Lemma pow_mod_help m a b : 1 < m -> (pow_mod m a b =? 1) = (eqmb m (a ^ b) 1).
proof: Proof. intros hm. rewrite pow_mod_spec. unfold eqmb. f_equal. rewrite Zmod_1_l; auto. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)