proposition: Lemma CRpower_N_bounded_weaken : forall (n:N) (c1 c2:Qpos) x, ((- (' (proj1_sig c1)) <= x /\ x <= 'proj1_sig c1) -> (proj1_sig c1 <= proj1_sig c2)%Q -> CRpower_N_bounded n c1 x == CRpower_N_bounded n c2 x)%CR.
proof: Proof. intros n c1 c2 x Hx Hc. simpl in x. rewrite <- CRpower_N_bounded_correct. rewrite <- CRpower_N_bounded_correct. reflexivity. 2: exact Hx. destruct Hx. split. - apply (@CRle_trans _ (-'(proj1_sig c1))%CR). apply CRopp_le_compat, CRle_Qle, Hc. exact H. - apply (CRle_trans H0). apply CRle_Qle, Hc. 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