proposition: Lemma eq_bigsetU_seqD F n : nondecreasing_seq F -> F n = \big[setU/set0]_(i < n.+1) seqD F i.
proof: Proof. move=> ndF; elim: n => [|n ih]; rewrite funeqE => x; rewrite propeqE; split. - by move=> ?; rewrite big_ord_recl big_ord0; left. - by rewrite big_ord_recl big_ord0 setU0. - rewrite (setU_seqD ndF) => -[|/=]. by rewrite big_ord_recr /= -ih => Fnx; left. by move=> -[Fn1x Fnx]; rewrite big_ord_recr /=; right. - by rewrite big_ord_recr /= -ih => -[|[]//]; move: x; exact/subsetPset/ndF. 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