proposition: Lemma Qmult_Z_plus_Z_dL : forall (a b : Z) (p : Qpositive), Qplus (Qmult (Z_to_Q a) (Qpos (dL p))) (Z_to_Q b) = Qmult (Qplus (Qmult (Z_to_Q (a + b)) (Qpos p)) (Z_to_Q b)) (Qinv (Qplus (Qpos p) Qone)).
proof: Proof. intros; rewrite Qmult_Z_dL. rewrite Z_to_Qplus; field; discriminate. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)