proposition: Lemma V2_Und2: y <> 0 -> alpha1 = 0 \/ bpow beta (emin + prec) <= Rabs alpha1.
proof: Proof. Proof with auto with typeclass_instances. intros Zy. unfold alpha1. assert (Fu2: format u2). replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). apply generic_format_opp. apply mult_error_FLT... intros L; case U1; intros H; try easy. apply Rle_trans with (2:=H); apply bpow_le. lia. case (Req_dec (round_flt (y + u2)) 0%R); intros L;[now left|right]. apply round_FLT_plus_ge... case U2; try easy; intros M. apply Rle_trans with (2:=M); apply bpow_le; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat