proposition: Lemma join1'_neq0 (s : necset {necset C}) : join1' s != set0 :> set _.
proof: Proof. rewrite hull_eq0 set0P. case/set0P: (neset_neq0 s) => y. case/set0P: (neset_neq0 y) => x yx sy. by exists x; exists y => //; move: sy; rewrite -in_setE => ->. Qed.
imports: Reals mathcomp(all_ssreflect) mathcomp(boolp classical_sets) mathcomp(finmap) infotheo(Reals_ext classical_sets_ext ssrR ssr_ext) infotheo(fdist fsdist convex necset) monae_lib HB(structures) category