apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0 ∧ 0 * 0 ≃ 0