proposition: Lemma pow_INR : forall m n:nat, INR (m ^ n) = pow (INR m) n.
proof: Proof. now intros m n; induction n as [| n IH]; [| simpl; rewrite mult_INR, IH]. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField