proposition: Lemma CRmax_ub_l : forall x y, (x <= CRmax x y)%CR.
proof: Proof. intros x y e. simpl. unfold Cap_raw. simpl. unfold Cap_raw. simpl. rewrite -> Qmax_plus_distr_l. eapply Qle_trans;[|apply Qmax_ub_l]. cut (QAbsSmall (proj1_sig e) (approximate x ((1 # 2) * ((1 # 2) * e))%Qpos + - approximate x ((1 # 2) * e)%Qpos));[unfold QAbsSmall;tauto|]. change (ball (proj1_sig e) (approximate x ((1 # 2) * ((1 # 2) * e))%Qpos) (approximate x ((1 # 2) * e)%Qpos)). eapply ball_weak_le;[|apply regFun_prf]. simpl. rewrite -> Qle_minus_iff. ring_simplify. apply (Qpos_nonneg ((2#8)*e)). Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names