proposition: Lemma spec_Qquadratic_Qpositive_to_Q_Zopp_2 : 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. apply Qmult_Qopp_left. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)