proposition: Lemma comp_separated (X Y Z : obj) (f : ele X -> ele Y) (g : ele Y -> ele Z) : separated f -> separated g -> separated (g \o f).
proof: Proof. move: f g. move: X Y Z => [X1 X2] [Y1 Y2] [Z1 Z2] f g [/= Hf1 Hf2] [/= Hg1 Hg2]; split=> x. - by case/cid: (Hf1 x)=> y /= ->; case/cid: (Hg1 y)=> z /= ->; exists z. - by case/cid: (Hf2 x)=> y /= ->; case/cid: (Hg2 y)=> z /= ->; exists z. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)