omega with nested ℕ division by 2^k: generalize the quotient first

Goal (n / 2^k + 1) / 2 = n / 2^k - n / 2^k / 2, which is true for any q = n / 2^k. omega failed and produced a bogus counterexample. It pushes the casts inconsistently: ↑(n / 2^k) becomes ↑n / ↑(2^k), while ↑(n / 2^k + 1) / 2 stays a separate atom, so the link is lost. Fix: generalize n / 2 ^ k = q and then omega succeeds immediately. Related rewriting chain for ⌊(n+2^k)/2^{k+1}⌋: rw [pow_succ, ← Nat.div_div_eq_div_mul, ← Nat.div_div_eq_div_mul, Nat.add_div_right _ (Nat.two_pow_pos k)]. Also note that Nat.pos_pow_of_pos no longer exists; use Nat.two_pow_pos or pow_pos.