proposition: Lemma bigsubsetU (P : set U) (X : U -> set T) (Y : set T) : (forall i, P i -> X i `<=` Y) <-> \bigcup_(i in P) X i `<=` Y.
proof: Proof. split. - by move=> H a [] i Pi Xia; apply (H i). - by move=> H i Pi a Xia; apply H; exists i. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp classical_sets)