let pm := p * m
ℕ : 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
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
ℕ : 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
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j