proposition: Lemma what_nR_does : forall p : Qpositive, nR p = Qpositive_plus p One.
proof: Proof. intros qp. unfold Qpositive_plus;fold Qpositive_plus. functional induction (Qpositive_plus qp One). rewrite e;rewrite e0. rename e into H_pq. rename e0 into H_p'q'. generalize (interp_non_zero qp). rename q0 into q. intros (p0', (q0', Hpq')). rewrite H_pq in Hpq'. let f_local := eval compute in (f_equal (fst (B:=_)) Hpq') in let g_local := eval compute in (sym_eq (f_equal (fst (B:=_)) H_p'q')) in generalize f_local g_local. let f_local := eval compute in (f_equal (snd (B:=_)) Hpq') in let g_local := eval compute in (sym_eq (f_equal (snd (B:=_)) H_p'q')) in generalize f_local g_local. intros Hq Hq' Hp Hp'. subst. rewrite <- (mult_n_Sm (S q0') 0). repeat rewrite <- plus_n_Sm. rewrite <- mult_n_O. rewrite plus_O_n. rewrite Nat.mul_1_l. rewrite Nat.mul_1_r. rewrite Qpositive_c_nR. rewrite Nat.add_sub. apply f_equal with Qpositive. symmetry in |- *; apply construct_correct. assumption. rewrite Nat.add_comm. apply Nat.le_add_r. clear; lia. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)