proposition: Lemma CRpower_N_bounded_N_power : forall (n : N) (c:Qpos) (x:CR), ((- (' (proj1_sig c)) <= x /\ x <= 'proj1_sig c) -> CRpower_N_bounded n c x == CRpower_N x n)%CR.
proof: Proof. intros n c x Hc. assert (- ('proj1_sig (CR_b (1#1) x)) <= x /\ x <= ('proj1_sig (CR_b (1#1) x)))%CR as Hx. { split. rewrite -> CRopp_Qopp. apply CR_b_lowerBound. apply CR_b_upperBound. } unfold CRpower_N. generalize (CR_b (1#1) x) Hx. clear Hx. intros d Hd. destruct (Qlt_le_dec (proj1_sig c) (proj1_sig d)). apply CRpower_N_bounded_weaken. exact Hc. apply Qlt_le_weak, q. symmetry. apply CRpower_N_bounded_weaken; assumption. 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