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