have : a//1 + b//1 ≃ (a + b)//1 := calc
  a//1 + b//1              ≃ _ := eqv_refl
  (a * 1 + 1 * b)//(1 * 1) ≃ _ := substN (AA.substL AA.identR)
  (a + 1 * b)//(1 * 1)     ≃ _ := substN (AA.substR AA.identL)
  (a + b)//(1 * 1)         ≃ _ := substD AA.identL
  (a + b)//1               ≃ _ := eqv_refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a + b)//1 ≃ a//1 + b//1
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
this : a//1 + b//1 ≃ (a + b)//1
⊢ (a + b)//1 ≃ a//1 + b//1