proposition: Lemma kleisli_fcomp A B C (f : A -> M B) (g : B -> A) (h : C -> M B) : ((f \o g) <=< h) = f <=< (g (o) h).
proof: Proof. by rewrite /kleisli fcomp_def functor_o 2!compA. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)