proposition: Theorem construct_correct4 : forall p q p' q' n n' : nat, S p + S q <= S n -> S p' + S q' <= S n' -> S p * S q' = S p' * S q -> Qpositive_c (S p) (S q) (S n) = Qpositive_c (S p') (S q') (S n').
proof: Proof. intros p q p' q' n n' H H0 H1. elim (construct_correct2 _ _ _ H). intros d (Heq1, Heq2). elim (construct_correct2 _ _ _ H0). intros d' (Heq3, Heq4). elim (interp_non_zero (Qpositive_c (S p) (S q) (S n))). intros p0 Hex1; elim Hex1; intros q0 Heq5; clear Hex1. elim (interp_non_zero (Qpositive_c (S p') (S q') (S n'))). intros p'0 Hex1; elim Hex1; intros q'0 Heq6; clear Hex1. elim (interp_reduced_fraction (Qpositive_c (S p) (S q) (S n))); intros a Hex1; elim Hex1; intros b; clear Hex1. rewrite Heq6 in Heq4; rewrite Heq6 in Heq3; rewrite Heq5 in Heq2; rewrite Heq5 in Heq1; rewrite Heq5; unfold fst, snd in |- *; intros Heq7. generalize H1; rewrite Heq1; rewrite Heq2; rewrite Heq3; rewrite Heq4; unfold fst, snd in |- *; clear H1; intros H1. unfold fst, snd in Heq1, Heq2, Heq3, Heq4. cut (S p0 * S q'0 = S p'0 * S q0). intros Heq8. cut (S p'0 = Z.abs_nat (a * S p'0 + b * S q'0) * S p0). intros Heq9. cut (S q'0 = Z.abs_nat (a * S p'0 + b * S q'0) * S q0). intros Heq10. cut (exists d'' : nat, Z.abs_nat (a * S p'0 + b * S q'0) = S d''). intros Hex; elim Hex; intros d'' Heq11; rewrite Heq11 in Heq9; rewrite Heq11 in Heq10. replace (S p0 * S d) with (S (d + p0 * S d)). replace (S q0 * S d) with (S (d + q0 * S d)). rewrite (construct_correct3 n n (d + p0 * S d) (d + q0 * S d) (S p0) (S q0) d). replace (S p'0 * S d') with (S (d' + p'0 * S d')). replace (S q'0 * S d') with (S (d' + q'0 * S d')). symmetry in |- *. apply construct_correct3 with (d := d' + d'' * S d'). replace (S (d' + p'0 * S d')) with (S p'0 * S d'). rewrite Heq9; ring. auto. replace (S (d' + q'0 * S d')) with (S q'0 * S d'). rewrite Heq10; ring. auto. replace (S (d' + q'0 * S d')) with (S q'0 * S d'). replace (S (d' + p'0 * S d')) with (S p'0 * S d'). rewrite <- Heq3; rewrite <- Heq4. exact H0. auto. auto. apply Nat.le_trans with (S p + S q). rewrite Heq1; rewrite Heq2. rewrite <- Nat.mul_add_distr_r. rewrite Nat.mul_comm; simpl in |- *; auto with arith. assumption. auto. auto. rewrite (Nat.mul_comm (S d)); auto. rewrite (Nat.mul_comm (S d)); auto. replace (S (d + q0 * S d)) with (S q0 * S d). replace (S (d + p0 * S d)) with (S p0 * S d). rewrite <- Heq1; rewrite <- Heq2. exact H. auto. auto. apply Nat.le_trans with (S p + S q). rewrite Heq1; rewrite Heq2. rewrite <- Nat.mul_add_distr_r. rewrite Nat.mul_comm; simpl in |- *; auto with arith. assumption. auto. auto. CaseEq (Z.abs_nat (a * S p'0 + b * S q'0)). intros Dummy; rewrite Dummy in Heq10; simpl in Heq10; discriminate Heq10. intros d'' Heq; exists d''; auto. rewrite <- (absolu_inj_nat (S q0)). pattern (S q'0) at 1 in |- *; rewrite <- (absolu_inj_nat (S q'0)). rewrite <- absolu_mult. apply f_equal with (f := Z.abs_nat). pattern (Z_of_nat (S q'0)) at 1 in |- *; rewrite <- Zmult_1_r. rewrite <- Heq7. replace (S q'0 * (a * S p0 + b * S q0))%Z with (S p0 * S q'0 * a + S q'0 * (b * S q0))%Z. rewrite <- (Znat.inj_mult (S p0)). rewrite Heq8. rewrite Znat.inj_mult; ring. ring. rewrite <- (absolu_inj_nat (S p0)). pattern (S p'0) at 1 in |- *; rewrite <- absolu_inj_nat. rewrite <- absolu_mult. apply f_equal with (f := Z.abs_nat). pattern (Z_of_nat (S p'0)) at 1 in |- *; rewrite <- Zmult_1_r. rewrite <- Heq7. replace (S p'0 * (a * S p0 + b * S q0))%Z with (S p'0 * S q0 * b + S p'0 * (a * S p0))%Z. rewrite <- (Znat.inj_mult (S p'0)). rewrite <- Heq8. rewrite Znat.inj_mult; ring. ring. apply mult_reg_l with (d' + d * S d'). replace (S (d' + d * S d')) with (S d * S d'). transitivity (S p0 * S d * (S q'0 * S d')). ring. rewrite H1. ring. auto. Qed.