proposition: Lemma eq_bigcup_seqD F : \bigcup_n F n = \bigcup_n seqD F n.
proof: Proof. rewrite funeqE => x; rewrite propeqE; split. case; elim=> [_ F0x|n ih _ Fn1x]; first by exists O. have [|Fnx] := pselect (F n x); last by exists n.+1. by move=> /(ih I)[m _ Fmx]; exists m. case; elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; by [exists O | exists n.+1]. 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