proposition: Lemma bigcup_seq r F : \bigcup_(i <- r) F i = \bigcup_(i in r) F i.
proof: Proof. elim: r => [|i r IHr]; first by rewrite big_nil big_pred0. rewrite big_cons {}IHr; case r_i: (i \in r). rewrite (setUidPr _) ?bigcup_sup //. by apply: eq_bigl => j /[!inE]; case: eqP => // ->. rewrite (bigD1 i (mem_head i r)) /=; congr (_ :|: _). by apply: eq_bigl => j /=; rewrite andbC; case: eqP => // ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)