proposition: Lemma bigcupC T U V A B (F : T -> U -> set V) : \bigcup_(i in A) \bigcup_(j in B) F i j <--> \bigcup_(j in B) \bigcup_(i in A) F i j.
proof: Proof. wlog suff: T U A B F / \bigcup_(i in A) \bigcup_(j in B) F i j \subset \bigcup_(j in B) \bigcup_(i in A) F i j. by move=> sub; apply/subset_eqP; split; apply: sub. by move=> x [i [Ai [j [Bj ?]]]]; exists j; split=> //; exists i. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)