rw [‹2*n.succ - 1 = 2 * (n.succ - 1) + 1›, this]
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * (succ n - 1)