proposition: Lemma bigcup_setX (E : I -> {set A}) (F : {set B}) : \bigcup_(i in I) (F `* E i) = F `* (\bigcup_(i in I) (E i)).
proof: Proof. apply/setP => -[b a] /=; rewrite !inE /=. apply/bigcupP/andP => [[/= i _]|[K1] /bigcupP[/= i _ aEi]]. rewrite !inE /= => /andP[xb yai]; rewrite xb; split => //. by apply/bigcupP; exists i. by exists i => //; rewrite !inE /= K1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext