proposition: Lemma biglub_iter_conv_set (X : neset L) (n : nat) : |_| (iter_conv_set X n)%:ne = |_| X.
proof: Proof. elim: n => [|n IHn /=]; first by congr (|_| _); apply/neset_ext. rewrite (biglub_oplus_conv_setE _ (iter_conv_set X n)%:ne). transitivity (|_| [set |_| X]%:ne); last by rewrite biglub1. congr (|_| _%:ne); apply/neset_ext => /=. transitivity ((fun _ => |_| X) @` probset); last by rewrite image_const. by congr image; apply funext=> p; rewrite IHn convmm. 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