proposition: Lemma fcomp_kleisli A B C D (f : A -> B) (g : C -> M A) (h : D -> M C) : f (o) (g <=< h) = (f (o) g) <=< h.
proof: Proof. rewrite /kleisli 2!fcomp_def 2!(compA (fmap f)) natural [in RHS]functor_o. by rewrite -compA. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)