proposition: Lemma bigcup_preimset (P : pred I) (F : A -> B) (E : I -> {set B}) : \bigcup_(i | P i) F @^-1: E i = F @^-1: \bigcup_(i | P i) E i.
proof: Proof. rewrite/preimset. apply/setP=> x; rewrite inE; apply/bigcupP/bigcupP => -[] i HPi; rewrite ?inE => HFxEi; exists i => //=; by rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext