calc
  a * 0 + 0 * b ≃ _ := AA.substL AA.absorbR
  0 + 0 * b     ≃ _ := AA.identL
  0 * b         ≃ _ := AA.absorbL
  0             ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0
no goals