proposition: Lemma Z_to_Qplus_POS_NEG : forall p1 p2 : positive, Z_to_Q (Zpos p1 + Zneg p2) = Qplus (Z_to_Q (Zpos p1)) (Z_to_Q (Zneg p2)).
proof: Proof. intros p1 p2. assert (H : Qplus (Z_to_Q (Zpos p1 + Zneg p2)) (Z_to_Q (Zpos p2)) = Z_to_Q (Zpos p1)). set (P := (Zpos p1 + Zneg p2)%Z) in *. assert (P = (Zpos p1 + Zneg p2)%Z); trivial. destruct P. unfold Z_to_Q at 1 in |- *. rewrite Qplus_zero_left. apply f_equal with Z. transitivity (- Zneg p2)%Z; trivial. lia. rewrite <- Z_to_Qplus_POS. apply f_equal with Z. replace (Zpos p2) with (- Zneg p2)%Z; trivial. lia. unfold Z_to_Q at 1 2 3 in |- *. assert (Hp : (Zpos p < Zpos p2)%Z). apply Zmin_cancel_Zlt. unfold Z.opp in |- *. rewrite H. rewrite <- (Zplus_0_l (Zneg p2)). apply Zplus_lt_compat_r. constructor. unfold Qplus in |- *. case (Qpositive_le_dec (Qpositive_c (nat_of_P p) 1 (S (nat_of_P p))) (Qpositive_c (nat_of_P p2) 1 (S (nat_of_P p2)))); intro H1. case (Qpositive_eq_dec (Qpositive_c (nat_of_P p) 1 (S (nat_of_P p))) (Qpositive_c (nat_of_P p2) 1 (S (nat_of_P p2)))); intro H2. apply False_ind. generalize (f_equal Qpositive_to_Z H2). do 2 rewrite Qpositive_to_Z_is_integer_part. apply Zorder.Zlt_not_eq; assumption. assert (Hp' : Zpos p2 = (Zpos p1 + Zpos p)%Z). clear H1 H2. replace (Zpos p) with (- Zneg p)%Z; trivial. rewrite H. replace (Zneg p2) with (- Zpos p2)%Z; trivial. auto with zarith. rewrite <- BinInt.Zpos_plus_distr in Hp'. generalize (POS_resp_eq _ _ Hp'). intro Hp2. apply f_equal with Qpositive. unfold Qpositive_sub in |- *. repeat rewrite Qpositive_i_c. repeat rewrite Nat.mul_1_l. repeat rewrite Nat.mul_1_r. clear H1 H2; apply Qpositive_c_equal_strong; trivial; try lia; rewrite Hp2; rewrite nat_of_P_plus_morphism. lia. lia. replace (nat_of_P p1 + nat_of_P p - nat_of_P p) with (nat_of_P p1); [ apply lt_O_nat_of_P | lia ]. lia. apply False_ind; apply H1. apply Qpositive_to_Z_Qpositive_le. do 2 rewrite Qpositive_to_Z_is_integer_part. assumption. rewrite <- H. replace (Zneg p2) with (- Zpos p2)%Z; trivial. rewrite Z_to_Qopp. ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)