proposition: Theorem construct_correct2 : forall n p q : nat, S p + S q <= n -> exists d : nat, S p = fst (Qpositive_i (Qpositive_c (S p) (S q) n)) * S d /\ S q = snd (Qpositive_i (Qpositive_c (S p) (S q) n)) * S d.
proof: Proof. intros n; elim n. intros p q Hle; inversion Hle. clear n; intros n. intros Hrec p q Hle; case (le_gt_dec (S p) (S q)). simpl in |- *. intros Hle'; rewrite (le_minus_O p q). CaseEq (q - p). intros Heq_minus; exists p. simpl in |- *; split; auto with arith. rewrite <- plus_n_O. apply Nat.le_antisymm; auto with arith. apply minus_O_le. auto. intros q' Heq_minus; elim (Hrec p q'). intros d; simpl in |- *; case (Qpositive_i (Qpositive_c (S p) (S q') n)); repeat rewrite <- (Nat.mul_comm (S d)); intros p'' q'' (Heq1, Heq2). exists d; split. exact Heq1. rewrite <- (Nat.sub_add (S p) (S q)). simpl in |- *. rewrite Heq_minus; rewrite Heq2. simpl in |- *. replace (S (p + q'' * S d)) with (S p + q'' * S d). rewrite Heq1. simpl in |- *. ring. simpl in |- *; auto. auto with arith. apply le_S_n. rewrite plus_n_Sm. apply Nat.le_trans with (S p + S q). apply Nat.add_le_mono_l. apply le_n_S. rewrite <- Heq_minus; apply minus_le. exact Hle. auto with arith. intros Hgt; simpl in |- *; CaseEq (p - q). intros H; apply Nat.lt_nge in Hgt. contradict Hgt. apply le_n_S. apply minus_O_le. exact H. intros p'. intros Heq_minus; simpl in |- *; elim (Hrec p' q). intros d; case (Qpositive_i (Qpositive_c (S p') (S q) n)). simpl in |- *; intros p'' q'' (Heq1, Heq2). exists d; split; auto. rewrite <- (Nat.sub_add (S q) (S p)); simpl in |- *. rewrite Heq_minus. replace (S (q + S p')) with (S q + S p'). rewrite Heq2; rewrite Heq1; ring. simpl in |- *; auto. auto with arith. rewrite <- Heq_minus. replace (p - q) with (S p - S q). rewrite (Nat.sub_add (S q) (S p)). apply Nat.le_trans with (S p + q). auto with arith. apply le_S_n; rewrite plus_n_Sm. exact Hle. auto with arith. auto. Qed.