proposition: Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k.
proof: Proof. rewrite /seqDU predeqE => t; split=> [[n _ Fnt]|[n _]]; last first. by rewrite setDE => -[? _]; exists n. have [UFnt|UFnt] := pselect ((\big[setU/set0]_(k < n) F k) t); last by exists n. suff [m [Fmt FNmt]] : exists m, F m t /\ forall k, (k < m)%N -> ~ F k t. by exists m => //; split => //; rewrite -bigcup_mkord => -[k kj]; exact: FNmt. move: UFnt; rewrite -bigcup_mkord => -[/= k _ Fkt] {Fnt n}. have [n kn] := ubnP k; elim: n => // n ih in t k Fkt kn *. case: k => [|k] in Fkt kn *; first by exists O. have [?|] := pselect (forall m, (m <= k)%N -> ~ F m t); first by exists k.+1. move=> /existsNP[i] /not_implyP[ik] /contrapT Fit; apply: (ih t i) => //. by rewrite (leq_ltn_trans ik). 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