show (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)