proposition: Lemma CR_b_upperBound : forall e x, (x <= 'proj1_sig (CR_b e x))%CR.
proof: Proof. intros e x e'. unfold CR_b. simpl. unfold Cap_raw. simpl. rewrite -> Qle_minus_iff. ring_simplify. destruct (regFun_prf x ((1#2)*e')%Qpos e) as [_ H]. simpl in H. rewrite -> Qle_minus_iff in H. ring_simplify in H. eapply Qle_trans. apply H. rewrite -> Qle_minus_iff. ring_simplify. clear H. apply Qabs_case; intros H. ring_simplify. apply (Qpos_nonneg ((1#2)*e')). apply (Qplus_le_r _ _ ((2#1)*approximate x e)). simpl. ring_simplify. apply (Qle_trans _ 0). rewrite <- (Qmult_0_r (2#1)). apply Qmult_le_l. reflexivity. exact H. apply (Qpos_nonneg ((1#2)*e')). Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names