proposition: Lemma biglub_hull (X : neset L) : |_| (hull X)%:ne = |_| X.
proof: Proof. transitivity (|_| (\bigcup_(i in natset) iter_conv_set X i)%:ne); first by congr (|_| _); apply neset_ext; rewrite /= hull_iter_conv_set. rewrite biglub_bignesetU /= -[in RHS](biglub1 (|_| X)). transitivity (|_| ((fun _ => |_| X) @` natset)%:ne); last first. by congr (|_| _); apply/neset_ext/image_const. congr (|_| _%:ne); apply/neset_ext => /=. rewrite image_comp; congr image; apply funext => n /=. by rewrite biglub_iter_conv_set. 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