proposition: Lemma natural_hcomp : naturality (F' \O F) (G' \O G) hcomp.
proof: Proof. move=> c0 c1 h. rewrite [in LHS]compA (natural t) -[in LHS]compA -[in RHS]compA; congr (_ \o _). rewrite [in RHS]FCompE -2!functor_o; congr (F' # _); apply hom_ext => /=. by rewrite natural. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)