unfold trunc ulp expt
case inl
n : ℕ
npos : 0 < n
x k : ℕ
eq_zero : x = 0
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
case inl
n : ℕ
npos : 0 < n
x k : ℕ
eq_zero : x = 0
⊢ 2 ^ k * x / 2 ^ (Nat.size (2 ^ k * x) - n) * 2 ^ (Nat.size (2 ^ k * x) - n) =
    2 ^ k * (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n))