proposition: Lemma frequencySizeMonotonic {A} (g0 : G A) lg : SizeMonotonic g0 -> List.Forall (fun p => SizeMonotonic (snd p)) lg -> SizeMonotonic (freq_ g0 lg).
proof: Proof. intros H1. unfold freq_. intros Hall. eapply bindMonotonicStrong. - eauto with typeclass_instances. - apply unsizedMonotonic. apply chooseUnsized. - intros x Heq. eapply semChoose in Heq; eauto. move : Heq => /andP [Hep1 Heq2]. destruct (sum_fst lg) eqn:Heq. + rewrite pick_def. eassumption. subst. ssromega. + edestruct (pick_exists lg x g0) as [[[n' g] [Hin [Hp Hg]]] H2]. rewrite Heq. unfold leq, RandomQC.super, ChooseNat, OrdNat in Hep1, Heq2. ssromega. eapply List.Forall_forall in Hall; [ | ]. eassumption. subst. rewrite Hp. eassumption. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)