have pos_mul_denom_prq : AP (Positive (pd * (rd * qd))) := inferInstance
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
pos_mul_denom_prq : AP (Positive (pd * (rd * qd)))
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd