proposition: Lemma arbNat_correct: semProd arbitrary <--> [set: nat].
proof: Proof. rewrite /arbitrary /=. rewrite semSized => n; split=> // _; exists n; split=> //. by rewrite (semChooseSize _ _ _) /RandomQC.leq /=. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)