proposition: Lemma semChooseEnum A `{RandomQC.ChoosableFromInterval A} (a1 a2 : A) : RandomQC.leq a1 a2 -> (semProd (choose (a1,a2)) <--> [set a | RandomQC.leq a1 a && RandomQC.leq a a2]).
proof: Proof. move=> /= le_a1a2. rewrite <- (unsized_alt_def 1). move => m /=. rewrite (enumRCorrect m 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)