calc
  (n + p) + (j + q) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (n + j) + (p + q) ≃ _ := AA.substL ‹n + j ≃ k + m›
  (k + m) + (p + q) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (k + p) + (m + q) ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n + p + (j + q) ≃ k + p + (m + q)
no goals