proposition: Lemma Qopp_linear : forall (a b : Z) (q : Qpositive), Qplus (Qmult (Z_to_Q (- a)) (Qpos q)) (Z_to_Q (- b)) = Qopp (Qplus (Qmult (Z_to_Q a) (Qpos q)) (Z_to_Q b)).
proof: Proof. intros a b q; 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; replace (Z_to_Q (-1)) with (Qopp Qone); [ ring | reflexivity ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)