unfold ulp expt
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ ulp n (2 ^ k * x) = 2 ^ k * ulp n x
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)