have : ∀ (k l : Nat), (2*k) &&& (2*l + 1) = 2*k &&& 2*l := by
  intro k l
  have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
  have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
  calc
    2*k &&& (2*l + 1)
      = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
    _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
    _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
    _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
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
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