intro (_ : p₁n//p₁d ≃ p₂n//p₂d)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d + qn//qd ≃ p₂n//p₂d + qn//qd
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n//p₁d + qn//qd ≃ p₂n//p₂d + qn//qd