unfold trunc
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
case inr.inl
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
lt_size : n < Nat.size x
⊢ 2 ^ k * x / ulp n (2 ^ k * x) * ulp n (2 ^ k * x) = 2 ^ k * (x / ulp n x * ulp n x)