proposition: Lemma semResizeEnum A n (g : E A) : semProd (resize n g) <--> semEnumSize g n .
proof: Proof. by case: g => g; rewrite /semProd /semProdSize /= /semEnumSize /= bigcup_const. 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)