have : (a₁ + c₂) + (b₂ + b₁) ≃ (c₁ + a₂) + (b₂ + b₁) := calc
  (a₁ + c₂) + (b₂ + b₁) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (a₁ + b₂) + (c₂ + b₁) ≃ _ := AA.substL ‹a₁ + b₂ ≃ b₁ + a₂›
  (b₁ + a₂) + (c₂ + b₁) ≃ _ := AA.substL AA.comm
  (a₂ + b₁) + (c₂ + b₁) ≃ _ := AA.substR AA.comm
  (a₂ + b₁) + (b₁ + c₂) ≃ _ := AA.substR ‹b₁ + c₂ ≃ c₁ + b₂›
  (a₂ + b₁) + (c₁ + b₂) ≃ _ := AA.comm
  (c₁ + b₂) + (a₂ + b₁) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (c₁ + a₂) + (b₂ + b₁) ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁ + c₂ ≃ c₁ + a₂
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
this : a₁ + c₂ + (b₂ + b₁) ≃ c₁ + a₂ + (b₂ + b₁)
⊢ a₁ + c₂ ≃ c₁ + a₂