proposition: Lemma triL1 : TriangularLaws.left eta1 eps1.
proof: Proof. move=> c; apply funext => x /=; apply/necset_ext => /=. rewrite eps1E /= free_semiCompSemiLattConvType_morE' /=. rewrite -[in RHS](hull_cset x); congr hull. rewrite eqEsubset eta1E; split=> a. - by case=> y [] b xb <-; rewrite necset1E => ->. - by move=> xa; exists (necset1 a); [exists a | rewrite necset1E]. 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