proposition: Lemma Qpositive_i_nR : forall (w : Qpositive) (p q : nat), Qpositive_i w = (p, q) -> Qpositive_i (nR w) = (p + q, q).
proof: Proof. intros w p q H_w; generalize (Qpositive_i_nR_with_let w); rewrite H_w; trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)