proposition: Lemma Z_to_Qplus_POS : forall p1 p2 : positive, Z_to_Q (Zpos p1 + Zpos p2) = Qplus (Z_to_Q (Zpos p1)) (Z_to_Q (Zpos p2)).
proof: Proof. intros p1 p2. unfold Z_to_Q at 2 3 in |- *. unfold Qplus in |- *. rewrite <- BinInt.Zpos_plus_distr. unfold Z_to_Q at 1 in |- *. apply f_equal with Qpositive. unfold Qpositive_plus in |- *. repeat rewrite Qpositive_i_c. repeat rewrite Nat.mul_1_l. repeat rewrite Nat.mul_1_r. apply f_equal3 with nat nat nat; trivial. apply nat_of_P_plus_morphism. rewrite nat_of_P_plus_morphism. lia. apply lt_O_nat_of_P. constructor. apply lt_O_nat_of_P. constructor. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)