fact: Definition Qeq_opp_r : ∀ x y, x == y → - x == - y := λ x y Hxy, let H₁ := eq_sym (f_equal Z.opp Hxy) in let H₂ := eq_trans (Z.mul_opp_l (Qnum y) (Zpos (Qden x))) H₁ in let H₃ := Z.mul_opp_l (Qnum x) (Zpos (Qden y)) in eq_trans H₃ (eq_sym H₂).
imports: Utf8 QArith NPeano Sorted Psatz