proposition: Lemma spec_Qquadratic_Qpositive_to_Q_Zopp_3 : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), spec_Qquadratic_Qpositive_to_Q a b c d (- e) (- f) (- g) (- h) p1 p2 = Qopp (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2).
proof: Proof. intros a b c d e f g h p1 p2; unfold spec_Qquadratic_Qpositive_to_Q in |- *; repeat rewrite Z_to_Qopp; repeat rewrite Qmult_Qopp_left; repeat rewrite <- Qopp_plus; rewrite Qinv_Qopp; rewrite Qmult_sym; rewrite Qmult_Qopp_left; rewrite Qmult_sym; reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)