proposition: Lemma ext_to_prod_comp A B C A' B' C' f g f' g': inc f (functions A B) -> inc f' (functions A' B') -> inc g (functions B C) -> inc g' (functions B' C') -> (g \ftimes g') \co (f \ftimes f') = (g \co f) \ftimes (g' \co f').
proof: Proof. move => /functionsP[ff _ tf]/functionsP[ff' _ tf']. move => /functionsP[fg sg _]/functionsP[fg' sg' _]. apply: compose_ext_to_prod2; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)