proposition: Theorem construct_correct3 : forall n n' p q p' q' d : nat, S p = S d * p' -> S q = S d * q' -> S p + S q <= S n -> p' + q' <= S n' -> Qpositive_c (S p) (S q) (S n) = Qpositive_c p' q' (S n').
proof: Proof. intros n; elim n; clear n. intros n' p q p' q' d; rewrite <- plus_n_Sm. simpl in |- *. intros H1 H2 H3; inversion H3. inversion H0. intros n0 Hrec n' p q p' q' d Heqd1 Heqd2 Hle1 Hle2. simpl in |- *. CaseEq (p - q). CaseEq (q - p). intros H H0. cut (p' = q'). intros Heq'; rewrite Heq'; rewrite (Nat.sub_diag q'). auto. apply mult_reg_l with d. rewrite <- Heqd2; rewrite <- Heqd1. apply Nat.le_antisymm; apply minus_O_le; assumption. intros q2 Heq2 Heqp. cut (p' <= q'). intros H; generalize (le_minus_O _ _ H). intros Heq3; rewrite Heq3. CaseEq (q' - p'). intros Heq4; cut (q' = p'). intros Heq5; generalize Heq2; replace (q - p) with (S q - S p). rewrite Heqd2; rewrite Heqd1; rewrite Heq5. rewrite Nat.sub_diag; intros Heq6; discriminate Heq6. auto. apply Nat.le_antisymm; apply minus_O_le; assumption. intros q'2. generalize Hle2; case n'. generalize Heqd1 Heqd2; case p'; case q'. simpl in |- *; intros H'1 H'2 H'3 H'4; discriminate H'4. intros x; rewrite <- (Nat.mul_comm 0); simpl in |- *; intros Dummy; discriminate Dummy. simpl in |- *; intros x H'1 H'2 H'3 H'4; discriminate H'4. simpl in |- *; intros n n1 H'1 H'2; rewrite <- plus_n_Sm; intros H'3; inversion H'3. inversion H1. intros n''. intros Hle3 Heq4. simpl in |- *. CaseEq p'. intros Heqp'; generalize Heqd1; rewrite Heqp'. rewrite <- (Nat.mul_comm 0); simpl in |- *; intros Dummy; discriminate Dummy. intros p'2 Heqp'2. change (dL (Qpositive_c (S p) (S q2) (S n0)) = dL (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *. apply f_equal with (f := dL). apply Hrec with d. - rewrite <- Heqp'2; assumption. - rewrite <- Heq4; rewrite <- Heq2; rewrite (Nat.mul_comm (S d)). rewrite Nat.mul_sub_distr_r. repeat rewrite <- (Nat.mul_comm (S d)). rewrite <- Heqd2; rewrite <- Heqd1. simpl in |- *; auto. - auto with zarith. - auto with zarith. - apply Nat.mul_le_mono_pos_l with (S d); auto with arith. rewrite <- Heqd2; rewrite <- Heqd1. apply le_n_S. apply minus_O_le; assumption. - intros p2 Heqp2. CaseEq (p' - q'). intros Heqm'; cut (S p - S q = 0). simpl in |- *; rewrite Heqp2; intros Dummy; discriminate Dummy. rewrite Heqd2; rewrite Heqd1. repeat rewrite (Nat.mul_comm (S d)). rewrite <- Nat.mul_sub_distr_r. rewrite Heqm'; simpl in |- *; auto. intros p'2. generalize Hle2; case n'. generalize Heqd1 Heqd2; case p'; case q'. simpl in |- *; intros H'1 H'2 H'3 H'4; discriminate H'4. intros x; rewrite <- (Nat.mul_comm 0); simpl in |- *; intros Dummy; discriminate Dummy. intros x; rewrite <- (Nat.mul_comm 0); simpl in |- *; intros Dummy1 Dummy2; discriminate Dummy2. simpl in |- *; intros n n1 H'1 H'2; rewrite <- plus_n_Sm; intros H'3; inversion H'3. inversion H0. intros n''. intros Hle3 Heq4. CaseEq q'. intros Heq5; generalize Heqd2; rewrite Heq5; simpl in |- *. rewrite <- (Nat.mul_comm 0); simpl in |- *; intros Dummy; discriminate Dummy. intros q'2 Heqq'2. change (nR (Qpositive_c (S p2) (S q) (S n0)) = nR (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *. apply f_equal with (f := nR). apply Hrec with d. * rewrite <- Heq4; rewrite <- Heqp2; rewrite (Nat.mul_comm (S d)). rewrite Nat.mul_sub_distr_r. repeat rewrite <- (Nat.mul_comm (S d)). rewrite <- Heqd2; rewrite <- Heqd1. simpl in |- *; auto. * rewrite <- Heqq'2; assumption. * auto with zarith. * auto with zarith. Qed.