have : (n ^^^ (n &&& k)) &&& (n &&& k) = 0 := by
  simp [←Nat.land_assoc n n k]
n k : Nat
⊢ n = (n ^^^ n &&& k) + (n &&& k)
n k : Nat
this : (n ^^^ n &&& k) &&& (n &&& k) = 0
⊢ n = (n ^^^ n &&& k) + (n &&& k)