proposition: Theorem Zfast_pow_pos_correct : forall v e, Zfast_pow_pos v e = Zpower_pos v e.
proof: Proof. intros v e. rewrite <- (Zmult_1_r (Zfast_pow_pos v e)). unfold Z.pow_pos. generalize 1%Z. revert v. induction e ; intros v f ; simpl. - rewrite <- 2!IHe. rewrite Z.square_spec. ring. - rewrite <- 2!IHe. rewrite Z.square_spec. apply eq_sym, Zmult_assoc. - apply eq_refl. Qed.
imports: Coq(ZArith Lia Zquot)