show (n * k + m * j)——(n * j + m * k) ≃ (k * n + j * m)——(k * m + j * n)
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ n——m * k——j ≃ k——j * n——m
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ (n * k + m * j)——(n * j + m * k) ≃ (k * n + j * m)——(k * m + j * n)