proposition: Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)).
proof: Proof. intros z; induction n as [| n IH]. - reflexivity. - rewrite Nat2Z.inj_succ, Z.pow_succ_r by (apply Nat2Z.is_nonneg). now simpl; rewrite IH, mult_IZR. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField