proposition: Lemma trivIset_seqDU F : trivIset setT (seqDU F).
proof: Proof. move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB ->. move=> /set0P; apply: contraNeq => _; apply/eqP. rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=. by rewrite setCU setIAC !setIA setICl !set0I. 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