proposition: Lemma Qpositive_i_nR_with_let : forall w : Qpositive, let (p, q) := Qpositive_i w in Qpositive_i (nR w) = (p + q, q).
proof: Proof. intros w;simpl Qpositive_i. functional induction (Qpositive_i w);subst;trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)