proposition: Lemma Qpos_nR : forall p : Qpositive, Qpos (nR p) = Qplus (Qpos p) Qone.
proof: Proof. intros. simpl in |- *. apply f_equal with Qpositive. apply what_nR_does. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)