proposition: Lemma iter_monotone_conv_set (X : neset A) (m : nat) : forall n, (m <= n)%N -> iter_conv_set X m `<=` iter_conv_set X n.
proof: Proof. elim: m => [n _|m IHm]. - case: n => // n. rewrite iter0_conv_set iterS_conv_set. by exists 1%:pr => //; rewrite conv1_set. - case => // n /(IHm _) mn. rewrite iterS_conv_set=> a [] p _ H. exists p => //. by move: (@conv_set_monotone p X _ _ mn) => /(_ a); apply. 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