proposition: Lemma CRpower_N_correct : forall (n:N) x, (CRpower_slow x (N.to_nat n) == CRpower_N x n)%CR.
proof: Proof. intros n x. rewrite <- (CRpower_N_bounded_N_power n (CR_b (1#1) x)). apply CRpower_N_bounded_correct. split. apply (CR_b_lowerBound (1#1) x). apply CR_b_upperBound. split. apply (CR_b_lowerBound (1#1) x). apply CR_b_upperBound. 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