intro (p₁n//p₁d)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → p₁ + q ≃ p₂ + q
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → p₁n//p₁d + q ≃ p₂ + q