proposition: Lemma biglubDl (p : {prob R}) (X : neset L) (y : L) : |_| X <|p|> y = |_| ((fun x => x <|p|> y) @` X)%:ne.
proof: Proof. rewrite convC biglubDr; congr (|_| _); apply/neset_ext/eq_imagel=> x ?. by rewrite -convC. 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