proposition: Lemma spec_Qhomographic_Qpositive_to_Q_Zopp_3 : forall (a b c d : Z) (q : Qpositive), spec_Qhomographic_Qpositive_to_Q a b (- c) (- d) q = Qopp (spec_Qhomographic_Qpositive_to_Q a b c d q).
proof: Proof. intros a b c d q; unfold spec_Qhomographic_Qpositive_to_Q in |- *; rewrite Qopp_linear; rewrite Qinv_Qopp; rewrite Qmult_sym; rewrite Qmult_Qopp_left; rewrite Qmult_sym; reflexivity. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)