proposition: Lemma bigsetU_seqD F n : \big[setU/set0]_(i < n) F i = \big[setU/set0]_(i < n) seqD F i.
proof: Proof. case: n => [|n]; first by rewrite 2!big_ord0. elim: n => [|n ih]; first by rewrite !big_ord_recl !big_ord0. rewrite big_ord_recr [in RHS]big_ord_recr /= -{}ih predeqE => x; split. move=> [?|?]; first by left. have [?|?] := pselect (F n x); last by right. by left; rewrite big_ord_recr /=; right. by move=> [?|[? ?]]; [left | 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