proposition: Lemma V2_Und4: a*x <> 0 -> beta1 = 0 \/ bpow beta (emin + prec+1) <= Rabs beta1.
proof: Proof. Proof with auto with typeclass_instances. intros Zax. unfold beta1; case U1; intros H. now contradict H. case (Req_dec (round_flt (u1 + alpha1)) 0%R); intros L;[now left|right]. apply round_FLT_plus_ge; try assumption... apply generic_format_round... apply generic_format_round... apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=H). apply bpow_le; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat