proposition: Theorem Qpositive_plus_1 : forall w : Qpositive, Qpositive_plus One w = nR w.
proof: Proof. intros w; elim (interp_non_zero w); intros p Hex; elim Hex; intros q Heq. unfold Qpositive_plus in |- *. replace (Qpositive_i One) with (1, 1). rewrite Heq. rewrite Nat.mul_1_r; rewrite Nat.mul_1_l. rewrite (Nat.add_comm (S q)). replace (S p + S q + S q) with (S (p + S q + S q)). rewrite (Qpositive_c_unfold1 p q). rewrite (construct_correct w); auto with *. auto. auto. auto. Qed.