proposition: Lemma arbInt_correctSize : semProd arbitrary <--> [set: Z].
proof: Proof. rewrite /arbitrarySized semSized => n; split=> // _; exists (Z.abs_nat n); split=> //. simpl. rewrite Nat2Z.inj_abs_nat (semChooseSize _ _ _). by case: n => //= p; rewrite !Z.leb_refl. apply/(Zle_bool_trans _ 0%Z); apply/Zle_is_le_bool. exact/Z.opp_nonpos_nonneg/Z.abs_nonneg. exact/Z.abs_nonneg. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)