have : 2 * n.succ - 1 = 2 * (n.succ - 1) + 1 := by
  simp only [Nat.mul_succ, Nat.succ_sub_one]
n : Nat
⊢ 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
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1