proposition: Lemma spec_Qhomographic_Qpositive_to_Q_Zopp : forall (a b c d : Z) (q : Qpositive), spec_Qhomographic_Qpositive_to_Q (- a) (- b) (- c) (- d) q = 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 |- *. repeat rewrite Zopp_eq_mult_neg_1. repeat rewrite Z_to_Qmult. repeat rewrite <- Qmult_assoc. rewrite (Qmult_sym (-1)%Z). repeat rewrite Qmult_assoc. repeat rewrite <- Q_distr_left. rewrite <- Qdiv_num_denom with (p := (-1)%Z). reflexivity. abstract discriminate. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)