have d : ulp n (2 ^ k * x) ∣ 2 ^ k * x := by
  unfold ulp expt
  apply dvd_mul_of_dvd_left
  rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
  rewrite [size_pow_mul (Nat.zero_lt_of_ne_zero ne_zero)]
  rewrite [tsub_le_iff_left]
  apply Nat.add_le_add_right
  exact size_le
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
d : ulp n (2 ^ k * x) ∣ 2 ^ k * x
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x