have expt_pos : 0 < (Nat.size x) - n := lt_tsub_of_add_lt_left no_uflow
case inl
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
⊢ round x = trunc n x
case inl
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
⊢ round x = trunc n x