proposition: Lemma Z_to_Qplus_NEG : forall p1 p2 : positive, Z_to_Q (Zneg p1 + Zneg p2) = Qplus (Z_to_Q (Zneg p1)) (Z_to_Q (Zneg p2)).
proof: Proof. intros p1 p2. replace (Zneg p1) with (- Zpos p1)%Z; trivial. replace (Zneg p2) with (- Zpos p2)%Z; trivial. rewrite <- Zopp_plus_distr. repeat rewrite Z_to_Qopp. rewrite Z_to_Qplus_POS. ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)