proposition: Lemma round_plus_small_id: forall f h, format f -> (bpow (prec+emin) <= Rabs f) -> Rabs h <= /4* ulp_flt f -> round_flt (f+h) = f.
proof: Proof. intros f h Ff H1 H2. case (Rle_or_lt 0 f); intros V. case V; clear V; intros V. apply round_plus_small_id_aux; try assumption. rewrite Rabs_right in H1; try assumption. apply Rle_ge; now left. contradict H1. rewrite <- V, Rabs_R0. apply Rlt_not_le, bpow_gt_0. rewrite <- (Ropp_involutive f), <- (Ropp_involutive h). replace (--f + --h) with (-(-f+-h)) by ring. rewrite round_NE_opp. apply f_equal. apply round_plus_small_id_aux. now apply generic_format_opp. rewrite Rabs_left in H1; try assumption. auto with real. now rewrite Rabs_Ropp, ulp_opp. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)