proposition: Lemma semChooseSize A `{ChoosableFromInterval A} (a1 a2 : A) : RandomQC.leq a1 a2 -> forall size, semProdSize (choose (a1,a2)) size <--> [set a | RandomQC.leq a1 a && RandomQC.leq a a2].
proof: Proof. move=> /= le_a1a2 m n //=; rewrite (enumRCorrect n a1 a2) //=. Qed.
imports: ZArith List mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat) Numbers.BinNums Classes.RelationClasses ExtLib.Structures(Functor Applicative) QuickChick(Sets Tactics Producer LazyList RandomQC)