proposition: Lemma arbInt_correct s : semProdSize arbitrary s <--> [set z | (- Z.of_nat s <= z <= Z.of_nat s)%Z].
proof: Proof. rewrite semSizedSize semChooseSize. by move=> n; split=> [/andP|] [? ?]; [|apply/andP]; split; apply/Zle_is_le_bool. apply/(Zle_bool_trans _ 0%Z); apply/Zle_is_le_bool. exact/Z.opp_nonpos_nonneg/Zle_0_nat. exact/Zle_0_nat. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)