apply congr_arg (fun w => 2 ^ (w - n))
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ ulp n x = ulp n y
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ Nat.size x = Nat.size y