proposition: Lemma nesetU_bigcup T (I J : neset T) : (I `|` J)%:ne = (\bigcup_(i in [set I; J]) idfun i)%:ne.
proof: Proof. apply/neset_ext => /=; rewrite eqEsubset; split => x. by case=> Hx; [exists I => //; left | exists J => //; right]. by case=> K [] -> Hx; [left | right]. Qed.
imports: HB(structures) Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets Rstruct reals) mathcomp(finmap) Reals_ext realType_ext classical_sets_ext ssrR fdist fsdist convex