proposition: Lemma exercise3_9 f g h: function f -> function g -> function h-> source g = target f -> source h = target g -> bijection (g \co f) -> bijection (h \co g) -> [/\ bijection f, bijection g & bijection h].
proof: Proof. move=> ff fg fh sgtf shtg bgf bhg. have cgf : g \coP f by []. have chg : h \coP g by []. have ig: injection g. by move: bhg=>[ia sa]; apply: (right_compose_fi chg ia). have sg: surjection g. by move: bgf=>[ia sa]; apply: (left_compose_fs cgf sa). have bg: bijection g by split. split => //. apply: (right_compose_fb cgf bgf bg). apply: (left_compose_fb chg bhg bg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)