proposition: Lemma seqDUIE (S : set T) (F : (set T)^nat) : seqDU (fun n => S `&` F n) = (fun n => S `&` F n `\` \bigcup_(i < n) F i).
proof: Proof. apply/funext => n; rewrite -setIDA; apply/seteqP; split; last first. move=> x [Sx [Fnx UFx]]; split=> //; apply: contra_not UFx => /=. by rewrite bigcup_mkord -big_distrr/= => -[]. by rewrite /seqDU -setIDA bigcup_mkord -big_distrr/= setDIr setIUr setDIK set0U. 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