proposition: Lemma pow_mod_pos_spec m a n : pow_mod_pos m a n = (a ^ Z.pos n) mod m.
proof: Proof. revert a. induction n; intros a; simpl pow_mod_pos. - rewrite IHn. replace (Z.pos n~1) with (1 + 2 * Z.pos n) by lia. rewrite Z.pow_add_r; try lia. rewrite Z.pow_mul_r; try lia. replace (a ^ 2) with (a * a) by lia. replace (a ^ 1) with a by lia. rewrite <-Zpow_mod. rewrite Zmult_mod_idemp_r. reflexivity. - rewrite IHn. change (Z.pos n~0) with (2 * Z.pos n). rewrite Z.pow_mul_r; try lia. replace (a ^ 2) with (a * a) by lia. rewrite <-Zpow_mod. lia. - f_equal. lia. Qed.
imports: Coq(PArith ZArith Lia Znumtheory) Coqtail(Ztools)