proposition: Lemma ARtoCR_preserves_power_N (x : AR) (n : N) : cast AR CR (x ^ n) = ('x) ^ n.
proof: Proof. unfold pow, CRpower_N, ARpower_N. rewrite ARtoCR_preserves_power_N_bounded. apply Cmap_wd. 2: reflexivity. assert (QposEq (cast (AQ₊) (Q₊) (AR_b x)) (CR_b (1#1) ('x))). { unfold QposEq. simpl. now rewrite ARtoCR_approximate, <-AR_b_correct. } rewrite H5. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower MathClasses.implementations.stdlib_binary_naturals MathClasses.orders.minmax MathClasses.implementations.positive_semiring_elements CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.AQmetric