proposition: Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n.
proof: Proof. intros r n; destruct n as [|p]. - reflexivity. - simpl. unfold Z.pow_pos. replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring. generalize 1. induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing