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