proposition: Lemma bindmret_derived : BindLaws.right_neutral (bind_of_join join) ret.
proof: Proof. by move=> A m; rewrite /bind_of_join -(compE (@join _)) joinMret. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)