proposition: Lemma V1_Und3': u1 = 0 \/ bpow beta (emin + 2*prec-1) <= Rabs u1.
proof: Proof. Proof with auto with typeclass_instances. case V1_Und1; intros K. left; unfold u1. rewrite K; apply round_0... right; unfold u1. apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat