proposition: Lemma bindretf_derived : BindLaws.left_neutral (bind_of_join join) ret.
proof: Proof. move=> A B a f; rewrite /bind_of_join -(compE (@join _)) -(compE _ (@ret _)). by rewrite -compA (natural ret) compA joinretM compidf. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)