proposition: Lemma plus_error_le_l : forall x y, generic_format beta fexp x -> generic_format beta fexp y -> (Rabs (round beta fexp (Znearest choice) (x + y) - (x + y)) <= Rabs x)%R.
proof: Proof. intros x y Fx Fy. apply (Rle_trans _ (Rabs (y - (x + y)))); [now apply round_N_pt|]. rewrite Rabs_minus_sym; right; f_equal; ring. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative