proposition: Lemma semProdOpt_equiv {A} {G} `{PG: Producer G} (g : G (option A)) : semProdOpt g <--> \bigcup_s semProdSizeOpt g s.
proof: Proof. split; move => [n [Hn H]]; exists n; split; auto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)