proposition: Lemma ARpower_N_bounded_N_power (n : N) (x : AR) (c : AQ₊) : -'c ≤ x ≤ 'c → ARpower_N_bounded n c x = x ^ n.
proof: Proof. intros. apply (injective (cast AR CR)). rewrite ARtoCR_preserves_power_N, ARtoCR_preserves_power_N_bounded. destruct c as [c Pc]. apply CRpower_N_bounded_N_power. split. change (cast Q CR (-cast AQ Q c) ≤ cast AR CR x). rewrite <-rings.preserves_negate. rewrite <-ARtoCR_inject. apply (order_preserving _). intuition. change (cast AR CR x ≤ cast Q CR (cast AQ Q c)). rewrite <-ARtoCR_inject. apply (order_preserving _). intuition. 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