proposition: Theorem construct_correct2' : forall n p q : nat, 1 <= p -> 1 <= q -> p + q <= n -> exists d : nat, p = fst (Qpositive_i (Qpositive_c p q n)) * S d /\ q = snd (Qpositive_i (Qpositive_c p q n)) * S d.
proof: Proof. intros n p; case p. intros q H; inversion H. intros p' q; case q. intros Hle H; inversion H. intros q' Hle Hle2; exact (construct_correct2 n p' q'). Qed.