have uflow : x < 2 ^ n := by
  rewrite [← Nat.size_le]
  exact size_le.le
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
⊢ 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
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x