proposition: Lemma plus_error_le_r : forall x y, generic_format beta fexp x -> generic_format beta fexp y -> (Rabs (round beta fexp (Znearest choice) (x + y) - (x + y)) <= Rabs y)%R.
proof: Proof. now intros x y Fx Fy; rewrite Rplus_comm; apply plus_error_le_l. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative