proposition: Lemma bigsetU_seqDU F n : \big[setU/set0]_(k < n) F k = \big[setU/set0]_(k < n) seqDU F k.
proof: Proof. elim: n => [|n ih]; first by rewrite 2!big_ord0. rewrite !big_ord_recr /= predeqE => t; split=> [[Ft|Fnt]|[Ft|[Fnt Ft]]]. - by left; rewrite -ih. - have [?|?] := pselect ((\big[setU/set0]_(i < n) seqDU F i) t); first by left. by right; split => //; rewrite ih. - by left; rewrite ih. - by right. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau