proposition: Theorem construct_correct4' : forall p q p' q' n n' : nat, 1 <= p -> 1 <= q -> 1 <= p' -> 1 <= q' -> p + q <= n -> p' + q' <= n' -> p * q' = p' * q -> Qpositive_c p q n = Qpositive_c p' q' n'.
proof: Proof. intros p; case p. intros q p' q' n n' H; inversion H. intros p0 q; case q. intros p' q' n n' H H1; inversion H1. intros q0 p'; case p'. intros q' n n' H H1 H2; inversion H2. intros p'0 q'; case q'. intros n n' H H1 H2 H3; inversion H3. intros q'0 n; case n. simpl in |- *; intros n' H H1 H2 H3 H4; inversion H4. intros n0 n'; case n'. simpl in |- *; intros H H1 H2 H3 H4 H5; inversion H5. intros; apply construct_correct4; auto. Qed.