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