proposition: Theorem Qpositive_c_equiv : forall n p q n' p' q' : nat, S p + S q <= n -> S p' + S q' <= n' -> Qpositive_c (S p) (S q) n = Qpositive_c (S p') (S q') n' -> S p * S q' = S p' * S q.
proof: Proof. intros n; elim n. simpl in |- *; intros p q n' p' q' H; inversion H. intros n0 Hrec p q n'. case n'. simpl in |- *; intros p' q' H H1; inversion H1. unfold Qpositive_c in |- *. CaseEq (S p - S q). CaseEq (S q - S p). intros Heq1 Heq2 n1 p' q'; CaseEq (S p' - S q'). CaseEq (S q' - S p'). intros Heq3 Heq4; cut (p = q). intros Heq5; rewrite Heq5. cut (p' = q'). intros Heq6; rewrite Heq6. intros; apply Nat.mul_comm. apply eq_add_S; apply Nat.le_antisymm; apply minus_O_le; auto with *. apply eq_add_S; apply Nat.le_antisymm; apply minus_O_le; auto with *. intros p2 H H1 H2 H3 H4; discriminate H4. intros n2 H H1 H2 H4; discriminate H4. intros q2 Heq1 Heq2 n2 p' q'; CaseEq (S p' - S q'). CaseEq (S q' - S p'). intros H3 H4 H H1 H2; discriminate H2. intros q'2 H H1 H2 H3 H4; injection H4; intros H5. rewrite <- (Nat.sub_add (S p) (S q)). rewrite Nat.add_comm. rewrite <- (Nat.sub_add (S p') (S q')). rewrite Nat.add_comm. rewrite (Nat.mul_comm (S p)); rewrite (Nat.mul_comm (S p')). repeat rewrite Nat.mul_add_distr_r; repeat rewrite <- (Nat.mul_comm (S p)). apply f_equal with (f := fun x : nat => S p * S p' + x). rewrite Heq1; rewrite H. rewrite <- (Nat.mul_comm (S p')). apply Hrec with n2. rewrite <- Heq1. rewrite Nat.add_comm. rewrite Nat.sub_add. apply Nat.le_trans with (p + S q). auto with arith. apply le_S_n; exact H2. apply minus_O_le; auto. rewrite <- H. rewrite Nat.add_comm. rewrite Nat.sub_add. apply Nat.le_trans with (p' + S q'). auto with arith; fail. apply le_S_n; exact H3. apply minus_O_le; auto. exact H5. apply minus_O_le; auto. apply minus_O_le; auto. intros n1 dummy1 Dummy2 Dummy3 Dummy; discriminate Dummy. intros n1 Heq1 n2 p' q' Hle1 Hle2; CaseEq (S p' - S q'). CaseEq (S q' - S p'). intros Dummy3 Dummy1 Dummy2; discriminate Dummy2. intros n3 Dummy Dummy1 Dummy2; discriminate Dummy2. intros p'2 Heq2 Heq3. injection Heq3; clear Heq3; intros Heq3. rewrite <- (Nat.sub_add (S q) (S p)). rewrite Nat.add_comm. rewrite Heq1. rewrite <- (Nat.sub_add (S q') (S p')). rewrite <- (Nat.add_comm (S q')). rewrite Heq2. repeat rewrite Nat.mul_add_distr_r; repeat rewrite (Nat.mul_comm (S q')). apply f_equal with (f := fun x : nat => S q * S q' + x). apply Hrec with n2. rewrite Nat.add_comm; rewrite <- Heq1. rewrite Nat.add_comm. rewrite Nat.sub_add. apply Nat.le_trans with (p + S q). rewrite <- plus_n_Sm. auto with arith. apply le_S_n; assumption. lia. rewrite <- Heq2. rewrite Nat.sub_add. apply Nat.le_trans with (p' + S q'). rewrite <- plus_n_Sm; auto with arith. apply le_S_n; exact Hle2. lia. exact Heq3. lia. lia. Qed.