intro (pn//pd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q * r ≃ p * (q * r)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q * r ≃ pn//pd * (q * r)