proposition: Lemma biglub_flatten (F : neset (neset L)) : |_| (biglub @` F)%:ne = |_| (\bigcup_(i in F) idfun i)%:ne.
proof: Proof. rewrite biglub_bignesetU; congr (|_| _%:ne); apply/neset_ext => /=. by rewrite image_id. 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