proposition: Lemma CRle_abs : forall x:CR, (x <= CRabs x)%CR.
proof: Proof. intros x e1. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ (approximate x ((1 # 2) * e1)%Qpos + - approximate x ((1 # 2) * e1)%Qpos)). rewrite Qplus_opp_r. apply (Qopp_le_compat 0), Qpos_nonneg. apply Qplus_le_l. apply Qabs.Qle_Qabs. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Stability