proposition: Lemma naturality_join : naturality (M \O M) M join.
proof: Proof. rewrite /join => a b h. rewrite /M !FCompE -2!(functor_o G); congr (G # _). by rewrite hom_ext /= (natural eps). Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)