proposition: Lemma eq_bigcup_seqD_bigsetU F : \bigcup_n (seqD (fun n => \big[setU/set0]_(i < n.+1) F i) n) = \bigcup_n F n.
proof: Proof. rewrite -(@eq_bigcup_seqD (fun n => \big[setU/set0]_(i < n.+1) F i)). rewrite eqEsubset; split => [t [i _]|t [i _ Fit]]. by rewrite -bigcup_seq_cond => -[/= j _ Fjt]; exists j. by exists i => //; rewrite big_ord_recr /=; 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