intro k l
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l