proposition: Lemma bigcup_set1 (E : {set A}) : E = \bigcup_(a in E) [set a].
proof: Proof. apply/setP => a; apply/idP/bigcupP => [aE|[a' a'E]]. by exists a => //; rewrite inE. by rewrite inE => /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext