proposition: Lemma necset1_affine (C : convType) : affine (@necset1 C).
proof: Proof. move=> p a b /=; apply/necset_ext; rewrite eqEsubset; split=> x /=. - move->; rewrite necset_convType.convE. by apply conv_in_conv_set. - rewrite necset_convType.convE /necset1 /=. by case/conv_in_conv_set'=> a0 [] b0 [] -> [] -> ->. 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