proposition: Theorem plus_error : forall x y, format x -> format y -> format (round beta fexp (Znearest choice) (x + y) - (x + y))%R.
proof: Proof. intros x y Hx Hy. destruct (Zle_or_lt (cexp beta fexp x) (cexp beta fexp y)). now apply plus_error_aux. rewrite Rplus_comm. apply plus_error_aux ; try easy. now apply Zlt_le_weak. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative