proposition: Lemma hull_iter_conv_set (X : set A) : hull X = \bigcup_(i in natset) iter_conv_set X i.
proof: Proof. rewrite eqEsubset; split. by move=> x [] n [] g [] d [] gX ->; exists n => //; apply Convn_iter_conv_set. apply bigsubsetU. elim => [_|n IHn _]; first exact/subset_hull. have H : iter_conv_set X n.+1 `<=` oplus_conv_set X (hull X). exact/oplus_conv_set_monotone/IHn. apply (subset_trans H); rewrite oplus_convC_set. have : oplus_conv_set (hull X) X `<=` oplus_conv_set (hull X) (hull X). exact/oplus_conv_set_monotone/subset_hull. by move/subset_trans; apply; rewrite oplus_convmm_set_hull. 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