proposition: Lemma spec_Qquadratic_Qpositive_to_Q_spec_Qquadratic_Qpositive_to_Qpositive2_neg_1 : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), Qsgn (spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2) = (-1)%Z -> spec_Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 = Qneg (spec_Qquadratic_Qpositive_to_Qpositive2 (- a) (- b) (- c) (- d) e f g h p1 p2).
proof: Proof. intros a b c d e f g h p1 p2 H. unfold spec_Qquadratic_Qpositive_to_Q in |- *. unfold spec_Qquadratic_Qpositive_to_Qpositive2 in |- *. rewrite <- Q_tail_Qinv. rewrite <- Q_tail_Qmult. repeat rewrite Qopp_Qpos. rewrite <- Q_tail_Q_pos. repeat rewrite Z_to_Qopp. abstract ring. apply Qsgn_9. repeat rewrite Z_to_Qopp. repeat rewrite Qmult_Qopp_left. repeat rewrite <- Qopp_plus. rewrite Qmult_Qopp_left. rewrite Qsgn_25. unfold spec_Qquadratic_Qpositive_to_Q in H. rewrite H. constructor. repeat rewrite Z_to_Qopp. repeat rewrite Qmult_Qopp_left. repeat rewrite <- Qopp_plus. apply Qopp_resp_nonzero. intro H_absurd. unfold spec_Qquadratic_Qpositive_to_Q in H. rewrite H_absurd in H. discriminate H. intro H_absurd. unfold spec_Qquadratic_Qpositive_to_Q in H. rewrite H_absurd in H. rewrite Qmult_sym in H. discriminate H. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)