proposition: Lemma plus_eq_minus (x y z : R) : x + y = z <-> x = z - y.
proof: Proof. split; intro A. + apply (right_cancellation (+) y). now rewrite <- plus_assoc, rings.plus_negate_l, rings.plus_0_r. + apply (right_cancellation (+) (-y)). now rewrite <- plus_assoc, rings.plus_negate_r, rings.plus_0_r. 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