proposition: Lemma hombnd_sub_init : forall u v, generic_format radix2 fxp u -> generic_format radix2 fxp v -> hombnd' (Bmin (-1074) 53) (Rabs (u - v)) (sub u v) (u - v) (Float radix2 1 (-53)) (Float radix2 1 0).
proof: Proof. intros u v Fu Fv. split. now apply F2R_ge_0. unfold F2R at 1 3 ; simpl. rewrite 2!Rmult_1_l. repeat split ; try apply Rle_refl. unfold sub. destruct (Rle_or_lt (Rabs (u - v)) (bpow radix2 (53 + -1074))) as [S|S]. rewrite round_generic. unfold Rminus at 1. rewrite Rplus_opp_r, Rabs_R0. apply Rmult_le_pos. now apply F2R_ge_0. apply Rabs_pos. apply valid_rnd_N. apply FLT_format_plus_small ; try easy. now apply generic_format_opp. replace (F2R (Float radix2 1 (-53))) with (bpow radix2 (-1) * bpow radix2 (-53 + 1))%R. apply relative_error_N_FLT. easy. apply Rlt_le. apply Rle_lt_trans with (2 := S). now apply bpow_le. rewrite <- bpow_plus. unfold F2R. rewrite Rmult_1_l. now apply f_equal. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)