proposition: Lemma CRplus_0_l (x: CR): (0 + x == x)%CR.
proof: Proof. intros e1 e2. destruct x; simpl. unfold Cap_raw; simpl. rewrite Qplus_0_r. rewrite Qplus_0_l. assert ((1#2)*`e1 + `e2 <= `e1 + `e2)%Q. { apply Qplus_le_l. rewrite <- (Qmult_1_l (`e1)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. } apply (ball_weak_le Q_as_MetricSpace _ _ H), (regFun_prf ((1#2)*e1)%Qpos e2). Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders