no goals
n₁ n₂ d₁ d₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ n₁ /. d₁ - n₂ /. d₂ = (n₁ * d₂ - n₂ * d₁) /. (d₁ * d₂)
simp only [Rat.sub_eq_add_neg, neg_divInt,
  divInt_add_divInt _ _ z₁ z₂, Int.neg_mul, Int.sub_eq_add_neg]