proposition: Lemma spec_Qhomographic_Qpositive_to_Q_spec_ni2_neg_1 : forall (a b c d : Z) (q : Qpositive), Qsgn (spec_Qhomographic_Qpositive_to_Q a b c d q) = (-1)%Z -> spec_Qhomographic_Qpositive_to_Q a b c d q = Qneg (spec_ni2 (- a) (- b) c d q).
proof: Proof. intros a b c d p H. unfold spec_Qhomographic_Qpositive_to_Q in |- *. unfold spec_ni2 in |- *. rewrite <- Q_tail_Qinv. rewrite <- Q_tail_Qmult. rewrite Qopp_Qpos. rewrite <- Q_tail_Q_pos. rewrite Qopp_linear. abstract ring. apply Qsgn_9. rewrite Qopp_linear. rewrite Qmult_Qopp_left. rewrite Qsgn_25. unfold spec_Qhomographic_Qpositive_to_Q in H. rewrite H. constructor. rewrite Qopp_linear. apply Qopp_resp_nonzero. intro H_absurd. unfold spec_Qhomographic_Qpositive_to_Q in H. rewrite H_absurd in H. discriminate H. intro H_absurd. unfold spec_Qhomographic_Qpositive_to_Q in H. rewrite H_absurd in H. rewrite Qmult_sym in H. discriminate H. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)