proposition: Lemma CRabs_cases (P: CR -> Prop) {Pp: Proper (@msp_eq _ ==> iff) P} {Ps: forall x, Stable (P x)}: forall x, ((0 <= x -> P x) /\ (x <= 0 -> P (- x))) <-> P (CRabs x).
proof: Proof. Proof with auto. intros. apply from_DN. apply (DN_bind (CRle_dec x 0)). intro. apply DN_return. destruct H. rewrite (CRabs_neg _ c)... intuition. revert H. rewrite (proj2 (CRle_antisym x 0))... rewrite CRopp_0... rewrite (CRabs_pos _ c)... intuition. revert H. rewrite (proj2 (CRle_antisym x 0))... rewrite CRopp_0... 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