proposition: Lemma sepsnd_comp X Y Z (f : ele X -> ele Y) (g : ele Y -> ele Z) (Hf : separated f) (Hg : separated g) : sepsnd (comp_separated Hf Hg) = sepsnd Hg \o sepsnd Hf.
proof: Proof. apply funext=> x /=. suff: inr (A := el Z.1) (sepsnd (comp_separated Hf Hg) x) = inr (sepsnd Hg (sepsnd Hf x)) by case. by rewrite 3!sepsndK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)