proposition: Lemma comp_inhom X Y Z (f : ele X -> ele Y) (g : ele Y -> ele Z) : inhom f -> inhom g -> inhom (g \o f).
proof: Proof. move=> [] sf [] homfl homfr [] sg [] homgl homgr. exists (comp_separated sf sg). rewrite sepfst_comp sepsnd_comp; split; exact: funcomp_inhom. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)