apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
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, qn_pm * j + qm_pn * k) ≃ (q * nk_mj + p * nj_mk, 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
⊢ qn_pm * k + qm_pn * j ≃ q * nk_mj + p * nj_mk ∧ qn_pm * j + qm_pn * k ≃ q * nj_mk + p * nk_mj