rw[Hl]
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * b = 4 * (k * l)
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * (l + l) = 4 * (k * l)