proposition: Lemma CRpower_N_correct' : forall (n:nat) x, (CRpower_slow x n == CRpower_N x (N_of_nat n))%CR.
proof: Proof. intros n x. etransitivity; [| apply CRpower_N_correct]. now rewrite Nnat.nat_of_N_of_nat. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.reals.fast.CRArith Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax MathClasses.interfaces.canonical_names MathClasses.interfaces.additional_operations