proposition: Theorem Qpositive_c_equiv' : forall n p q n' p' q' : nat, 1 <= p -> 1 <= q -> 1 <= p' -> 1 <= q' -> p + q <= n -> p' + q' <= n' -> Qpositive_c p q n = Qpositive_c p' q' n' -> p * q' = p' * q.
proof: Proof. intros n p q n' p' q'; case p. intros H; inversion H. clear p; intros p Hlp. case q; [ intros H; inversion H | clear q; intros q Dummy; clear Dummy ]. case p'; [ intros H; inversion H | clear p'; intros p' Dummy; clear Dummy ]. case q'; [ intros H; inversion H | clear q'; intros q' Dummy; clear Dummy ]. intros; apply Qpositive_c_equiv with n n'; auto. Qed.