proposition: Lemma semFrequencySize {A} (l : list (nat * G A)) (def : G A) (size: nat) : semProdSize (freq_ def l) size <--> let l' := [seq x <- l | x.1 != 0] in if l' is nil then semProdSize def size else \bigcup_(x in l') semProdSize x.2 size.
proof: Proof. rewrite semBindSize semChooseSize //=. case lsupp: {1}[seq x <- l | x.1 != 0] => [|[n g] gs]. move/sum_fst_eq0P: lsupp => suml; rewrite suml. rewrite (@eq_bigcupl _ _ _ [set 0]) ?bigcup_set1 ?pick_def // ?leqn0 ?suml //. by move=> n; split; rewrite leqn0; [move/eqP|] => ->. symmetry; apply: reindex_bigcup. have pos_suml: 0 < sum_fst l. have [] := sum_fst_eq0P l. by rewrite lsupp; case: (sum_fst l) => // /(_ erefl). have->: (fun a : nat => a <= sum_fst l - 1) <--> [set m | m < sum_fst l]. by move=> m /=; rewrite -ltnS subn1 prednK. exact: pick_imset. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)