have distrib_swap (w x y z : ℕ)
    : q * (w + y) + p * (x + z) ≃ (q * w + p * x) + (q * y + p * z)
    := calc
  q * (w + y) + p * (x + z)         ≃ _ := AA.substL AA.distribL
  (q * w + q * y) + p * (x + z)     ≃ _ := AA.substR AA.distribL
  (q * w + q * y) + (p * x + p * z) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (q * w + p * x) + (q * y + p * z) ≃ _ := Rel.refl
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)