proposition: Lemma Qabs_cases : forall P : Q -> Prop, abs_cases_statement P.
proof: Proof. intros P Pp Ps x [? ?]. destruct (decide (0 ≤ x)) as [A | A]; [rewrite abs.abs_nonneg | apply le_flip in A; rewrite abs.abs_nonpos]; auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.stdlib_omissions.N CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.SimpleIntegration MathClasses.misc.propholds