proposition: Lemma etp_comp A B C f g: inc f (functions A B) -> inc g (functions B C) -> \Pof (g \co f) = (\Pof g) \co (\Pof f).
proof: Proof. move /functionsP => [[ff _ _] _ tf ] /functionsP [[fg _ _ ] sg _]. have cc: source g = target f by ue. by apply:(etp_compose). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)