proposition: Lemma ab_exact: round_flx (a-b)=a-b.
proof: Proof. Proof with auto with typeclass_instances. apply round_generic... apply sterbenz_aux... lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)