proposition: Lemma Qpos_dL : forall p : Qpositive, Qpos (dL p) = Qmult (Qpos p) (Qinv (Qplus (Qpos p) Qone)).
proof: Proof. intros. simpl in |- *. apply f_equal with Qpositive. apply what_dL_does. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)