proposition: Lemma spec_Qquadratic_Qpositive_to_Q_spec_Qquadratic_Qpositive_to_Qpositive2_pos : 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 = Qpos (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. rewrite <- Q_tail_Q_pos. reflexivity. apply Qsgn_9. assumption. 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)