proposition: Lemma CR_b_lowerBound : forall e x, (' (-proj1_sig (CR_b e x))%Q <= x)%CR.
proof: Proof. intros e x e'. unfold CR_b. simpl. unfold Cap_raw. simpl. rewrite -> Qle_minus_iff, Qopp_involutive, Qopp_involutive. destruct (regFun_prf x ((1#2)*e')%Qpos e) as [H _]. simpl in H. rewrite -> Qle_minus_iff in H. ring_simplify in H. apply (Qle_trans _ _ _ H). rewrite -> Qle_minus_iff. ring_simplify. clear H. apply Qabs_case; intros H. apply (Qle_trans _ (approximate x e + 0)). rewrite Qplus_0_r. exact H. rewrite <- Qplus_assoc. apply Qplus_le_r. apply (Qle_trans _ (0+approximate x e)). rewrite Qplus_0_l. exact H. apply Qplus_le_l. apply (Qpos_nonneg ((1#2)*e')). ring_simplify. 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