proposition: Lemma U5_discri1_aux : forall x y e, format x -> format y -> (emin <= e)%Z -> bpow e <= Rabs x -> bpow e <= Rabs y -> round_flt (x+y) <> x+y -> bpow e <= Rabs (round_flt (x+y)).
proof: Proof. Proof with auto with typeclass_instances. intros x y e Fx Fy He Hex Hey H. apply abs_round_ge_generic... apply generic_format_FLT_bpow... case (Rle_or_lt (bpow e) (Rabs (x+y))); intros H1; try easy. absurd (round_flt (x + y) = x + y); try assumption. apply round_generic... apply generic_format_plus... apply Rlt_le; apply Rlt_le_trans with (1:=H1). destruct (mag radix2 x) as (ex,Y1). destruct (mag radix2 y) as (ey,Y2); simpl. apply bpow_le. apply Z.min_glb. apply le_bpow with radix2. apply Rle_trans with (1:=Hex). apply Rlt_le, Y1. intros Zx; contradict H. rewrite Zx, Rplus_0_l, round_generic... apply le_bpow with radix2. apply Rle_trans with (1:=Hey). apply Rlt_le, Y2. intros Zy; contradict H. rewrite Zy, Rplus_0_r, round_generic... Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat