proposition: Lemma hom_compA (a b c d : C) (h : {hom c, d}) (g : {hom b, c}) (f : {hom a, b}) : (h \o g) \o f = [\o h, g, f] :> (el a -> el d).
proof: Proof. exact: compA. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)