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