proposition: Lemma slice_category_comp : forall (aa ba ca : slice) (f : el aa -> el ba) (g : el ba -> el ca), inhom f -> inhom g -> inhom (g \o f).
proof: Proof. by case=> aa haa [] ba hba [] ca hca /= f g -> ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)