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