have redistribute (x y : ℕ)
    : (q * n + p * m) * x + (q * m + p * n) * y
    ≃  q * (n * x + m * y) + p * (n * y + m * x)
    := calc
  (q * n + p * m) * x + (q * m + p * n) * y
    ≃ _ := AA.substL AA.distribR
  (q * n) * x + (p * m) * x + (q * m + p * n) * y
    ≃ _ := AA.substR AA.distribR
  (q * n) * x + (p * m) * x + ((q * m) * y + (p * n) * y)
    ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (q * n) * x + (q * m) * y + ((p * m) * x + (p * n) * y)
    ≃ _ := AA.substR AA.comm
  (q * n) * x + (q * m) * y + ((p * n) * y + (p * m) * x)
    ≃ _ := AA.substL (AA.substL AA.assoc)
  q * (n * x) + (q * m) * y + ((p * n) * y + (p * m) * x)
    ≃ _ := AA.substL (AA.substR AA.assoc)
  q * (n * x) + q * (m * y) + ((p * n) * y + (p * m) * x)
    ≃ _ := AA.substR (AA.substL AA.assoc)
  q * (n * x) + q * (m * y) + (p * (n * y) + (p * m) * x)
    ≃ _ := AA.substR (AA.substR AA.assoc)
  q * (n * x) + q * (m * y) + (p * (n * y) + p * (m * x))
    ≃ _ := AA.substL (Rel.symm AA.distribL)
  q * (n * x + m * y) + (p * (n * y) + p * (m * x))
    ≃ _ := AA.substR (Rel.symm AA.distribL)
  q * (n * x + m * y) + p * (n * y + m * x)
    ≃ _ := Rel.refl
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
qn_pm : ℕ := q * n + p * m
qm_pn : ℕ := q * m + p * n
nk_mj : ℕ := n * k + m * j
nj_mk : ℕ := n * j + m * k
redistribute : ∀ (x y : ℕ), (q * n + p * m) * x + (q * m + p * n) * y ≃ q * (n * x + m * y) + p * (n * y + m * x)
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj