proposition: Lemma V1_Und3: u1 = 0 \/ bpow beta (emin + prec) <= Rabs u1.
proof: Proof. case V1_Und3';[now left|right]. apply Rle_trans with (2:=H). apply bpow_le; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat