proposition: Lemma CRabs_opp (x: CR): CRabs (-x) == CRabs x.
proof: Proof. Proof with auto. intros. apply from_DN. apply (DN_bind (CRle_dec x 0)). intros [A | B]; apply DN_return. rewrite (CRabs_neg _ A). apply CRabs_pos. change (-0 <= -x). apply -> CRle_opp... rewrite (CRabs_pos _ B). rewrite CRabs_neg. apply CRopp_opp. change (-x <= -0). apply -> CRle_opp... 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