apply And.intro
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0 ∧ 0 * 0 ≃ 0
case left
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0

case right
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0