proposition: Lemma bigcup_setU A B F : \bigcup_(i in A :|: B) F i = (\bigcup_(i in A) F i) :|: (\bigcup_ (i in B) F i).
proof: Proof. apply/setP=> x; apply/bigcupP/setUP=> [[i] | ]. by case/setUP; [left | right]; apply/bigcupP; exists i. by case=> /bigcupP[i Pi]; exists i; rewrite // inE Pi ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)