proposition: Theorem c3f_fi u v: surjection u -> injection v -> injection (compose3function u v).
proof: Proof. rewrite /compose3function=> su iv. have fu: function u by fct_tac. have fv: function v by fct_tac. apply: lf_injective; first by apply: c3f_axiom. move=> f g. case: (emptyset_dichot (source v)) => sve. by move=> i1 i2 c; apply: (fun_set_small_target (x:= target u)); ue. have [s [cus cusi]] := (exists_right_inv_from_surj su). move: (exists_left_inv_from_inj iv sve). move=> [r [crv crvi]] /functionsP [ff sf tf] /functionsP [fg sg tg]. have cvf: v \coP f by []. have cvg: v \coP g by []. have fvf: function (v \co f) by fct_tac. have fvg: function (v \co g) by fct_tac. have cvfu: (v \co f) \coP u by hnf; aw. have cvgu: (v \co g) \coP u by hnf; aw. move/(congr1 (fun i => i \co s)). rewrite - compfA // cusi - sf - (compf_s f v) compf_id_r //. rewrite - compfA // cusi - sg - (compf_s g v) compf_id_r //. move /(congr1 (fun i => r \co i)). rewrite compfA // crvi - tf compf_id_l // compfA // crvi - tg compf_id_l //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)