proposition: Lemma Qmult_Z_nR : forall (a : Z) (p : Qpositive), Qmult (Z_to_Q a) (Qpos (nR p)) = Qplus (Qmult (Z_to_Q a) (Qpos p)) (Z_to_Q a).
proof: Proof. intros. rewrite Qpos_nR. ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)