fact: Definition freq_ {A : Type} (def : G A) (gs : list (nat * G A)) : G A := let tot := sum_fst gs in bindGen (choose (0, tot-1)) (fun n => @snd _ _ (pick def gs n)).
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)