proposition: Lemma JoinE T : (Join : (N \o N) T -> N T) = (Join : (M \o M) T -> M T).
proof: Proof. apply funext => t /=. rewrite /join_. rewrite [in LHS]/= HCompId HIdComp [X in _ (X t)]/=. rewrite /actm [in LHS]/=. rewrite epsCE. rewrite eps0_correct. rewrite /fsdistjoin /fsdistmap /= fsdistbindA /=. congr fsdistbind. by apply funext => x; rewrite fsdist1bind. 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 hierarchy