exact Nat.mul_lt_mul_of_pos_right h two_pos
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ x * 2 < (trunc n x + ulp n x / 2) * 2
no goals