proposition: Lemma F1join0'_neq0 X : (F1join0' X) != set0.
proof: Proof. apply/set0P. case/set0P: (neset_neq0 X) => x Xx. by exists (Convn_of_fsdist (x : {dist (F T)})), x. 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