proposition: Lemma semChooseSizeGen A `{ChoosableFromInterval A} (a1 a2 : A) : RandomQC.leq a1 a2 -> forall size, semGenSize (choose (a1,a2)) size <--> [set a | RandomQC.leq a1 a && RandomQC.leq a a2].
proof: Proof. by move=> /= le_a1a2 m n; rewrite (randomRCorrect n a1 a2). Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)