proposition: Corollary Beaulieu_technical_equality (x y : L): x [+] y = |_| ((fun p => x <| p |> y) @` probset)%:ne.
proof: Proof. rewrite lubE -[in LHS]biglub_hull; congr (|_| _); apply neset_ext => /=. rewrite eqEsubset; split=> i /=. - have /set0P x0 := set1_neq0 x. have /set0P y0 := set1_neq0 y. move/(@hull_setU _ _ (necset1 x) (necset1 y) x0 y0). by move=> [a /asboolP ->] [b /asboolP ->] [p ->]; exists p. - by case=> p ? <-; exact/mem_hull_setU. 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