. rewrite [ulp, expt, Nat.pow_dvd_pow_iff_le_right one_lt_two]
  exact tsub_le_self
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)