proposition: Lemma Qmult_Z_dL : forall (a : Z) (p : Qpositive), Qmult (Z_to_Q a) (Qpos (dL p)) = Qmult (Qmult (Z_to_Q a) (Qpos p)) (Qinv (Qplus (Qpos p) Qone)).
proof: Proof. intros. rewrite Qpos_dL. ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)