proposition: Lemma semElements {A} (l: list A) (def : A) : (semProd (elems_ def l)) <--> if l is nil then [set def] else l.
proof: Proof. rewrite /semProd; setoid_rewrite semElementsSize; rewrite bigcup_const //. by do 2! constructor. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)