proposition: Theorem Zpow_mod_pos_Zpower_pos_correct: forall a m n, 0 < n -> Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
proof: Proof. intros a m; elim m; simpl; auto. intros p Rec n H1; rewrite xI_succ_xO; rewrite Pplus_one_succ_r; rewrite <- Pplus_diag; auto. repeat rewrite Zpower_pos_is_exp; auto. repeat rewrite Rec; auto. replace (Zpower_pos a 1) with a; auto. 2: unfold Zpower_pos; simpl; auto with zarith. repeat rewrite (fun x => (Zmult_mod x a)); auto. rewrite (Zmult_mod (Zpower_pos a p)); auto. case (Zpower_pos a p mod n); auto. intros p Rec n H1; rewrite <- Pplus_diag; auto. repeat rewrite Zpower_pos_is_exp; auto. repeat rewrite Rec; auto. rewrite (Zmult_mod (Zpower_pos a p)); auto. case (Zpower_pos a p mod n); auto. unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic