intro (n——m)
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p : ℕ
⊢ ∀ {b : Difference ℕ}, q——p * b * c ≃ q——p * (b * c)
ℕ : Type
inst✝ : Natural ℕ
c : Difference ℕ
q p n m : ℕ
⊢ q——p * n——m * c ≃ q——p * (n——m * c)