calc
  (n * m + 0 * 0, n * 0 + 0 * m) ≃ _ := AA.substL (AA.substR AA.absorbL)
  (n * m + 0, n * 0 + 0 * m)     ≃ _ := AA.substL Natural.add_zero
  (n * m, n * 0 + 0 * m)         ≃ _ := AA.substR (AA.substL AA.absorbR)
  (n * m, 0 + 0 * m)             ≃ _ := AA.substR Natural.zero_add
  (n * m, 0 * m)                 ≃ _ := AA.substR AA.absorbL
  (n * m, 0)                     ≃ _ := Rel.refl
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m + 0 * 0, n * 0 + 0 * m) ≃ (n * m, 0)
no goals