proposition: Lemma semFrequency {A} (l : list (nat * G A)) (def : G A) : semProd (freq_ def l) <--> let l' := [seq x <- l | x.1 != 0] in if l' is nil then semProd def else \bigcup_(x in l') semProd x.2.
proof: Proof. by case lsupp: {1}[seq x <- l | x.1 != 0] => [|[n g] gs] /=; rewrite 1?bigcupC; apply: eq_bigcupr => sz; have := (semFrequencySize l def sz); rewrite lsupp. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)