proposition: Lemma err_opp: forall x y e, err x y e -> err (-x) (-y) e.
proof: Proof. intros x y e H. replace (-x - (-y)) with (-(x-y)) by ring. now rewrite 2!Rabs_Ropp. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)