proposition: Lemma arbNat_correctSize s : semProdSize arbitrary s <--> [set n : nat | (n <= s)%coq_nat].
proof: Proof. by rewrite semSizedSize semChooseSize // => n /=; case: leP. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)