proposition: Lemma Convn_iter_conv_set (n : nat) : forall (g : 'I_n -> A) (d : {fdist 'I_n}) (X : set A), g @` setT `<=` X -> iter_conv_set X n (<|>_d g).
proof: Proof. elim: n => [g d|n IHn g d X]; first by have := fdistI0_False d. have [/eqP ->|Xneq0 gX] := boolP (X == set0). by move=> /(_ (g ord0)) H; exfalso; apply/H/imageP. set X' := NESet.Pack (NESet.Mixin Xneq0). have gXi : forall i : 'I_n.+1, X (g i). by move=> i; move/subset_image : gX; apply. have [/eqP d01|d0n1] := boolP (d ord0 == 1). - suff : X (<|>_d g) by move/(@iter_conv_set_superset X' n.+1 (<|>_d g)). by rewrite (Convn_proj g d01); exact/gX/imageP. - rewrite ConvnIE //; exists (probfdist d ord0) => //; exists (g ord0) => //. rewrite conv_pt_setE. exists (<|>_(fdist_del d0n1) (fun x : 'I_n => g (fdist_del_idx ord0 x))) => //. by apply IHn => u [] i _ <-; exact/gX/imageP. 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