proposition: Theorem exists_right_composable f g: function f -> injection g -> target f = target g -> ((exists h, g \coP h /\ g \co h = f) <-> (sub (Imf f) (Imf g))).
proof: Proof. move=> ff ig tftg. have fg: function g by fct_tac. split. move => [h [chg cghf]] x /(Imf_P ff) [u usf ->]; apply/(Imf_P fg). have [_ fh th] := chg. move: usf; rewrite - cghf compf_s => usg; exists (Vf h u); [rewrite th; Wtac | rewrite compfV //]. case: (emptyset_dichot (source g)). case: (emptyset_dichot (source f)). move=> ssfe sge _. move: empty_function_function => [qa qb qc]. have cge: (g \coP empty_function) by split => //; rewrite qc. exists (empty_function); split=>//; symmetry. apply: function_exten;aw =>//;try fct_tac; rewrite ssfe ?qb //. move => x /in_set0 //. move=> [x xsf] sge hyp. move: (hyp _ (Imf_i ff xsf)); move/(Imf_P fg) => [u]. by rewrite sge => /in_set0. move=> nesg hyp. have [r rli]:= (exists_left_inv_from_inj ig nesg). have trsg:= (left_i_target rli). have [crg crgi] := rli. have crf: (r \coP f). by hnf; split => // ; first (by fct_tac); move: crg=> [_ _ ->]; symmetry. have fcrf: (function (r \co f)) by fct_tac. have cgrf: (g \coP (r \co f)) by hnf; aw. exists (r \co f); split=>//. symmetry;apply: function_exten;aw => //; first by fct_tac; aw. move=> x xsf. rewrite !compfV //; last by aw. have: (inc (Vf f x) (Imf g)) by apply: hyp; Wtac. move/(Imf_P fg) => [z zs ->]. have: (Vf (r \co g) z = z) by rewrite crgi idV. by rewrite compfV // => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)