proposition: Lemma bindaltDl : BindLaws.left_distributive (@hierarchy.bind gcm) alt.
proof: Proof. move=> A B x y k. rewrite hierarchy.bindE /= /join_ -category.bindE. by rewrite scsl_hom_is_lubmorph. Qed.
imports: Reals mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(boolp classical_sets) mathcomp(reals Rstruct) infotheo(classical_sets_ext Reals_ext ssrR fdist) infotheo(ssrR Reals_ext proba) infotheo(Reals_ext realType_ext) infotheo(fsdist convex necset) HB(structures) monae_lib hierarchy monad_lib proba_lib monad_model gcm_model category