proposition: Lemma Qpower_mc_power (e : Q) (n : nat) : (e ^ n)%Q = (e ^ n)%mc.
proof: Proof. induction n as [| n IH] using nat_induction. + now rewrite nat_pow_0. + rewrite Nat2Z.inj_add, Qpower_plus'. - now rewrite nat_pow_S, IH. - rewrite <- Nat2Z.inj_add; change 0%Z with (Z.of_nat 0); rewrite Nat2Z.inj_iff; apply not_eq_sym, O_S. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.implementations.stdlib_rationals CoRN.model.structures.Qinf CoRN.model.structures.Qpossec CoRN.model.structures.QposInf CoRN.model.structures.QnonNeg MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum CoRN.ode.metric