proposition: Theorem right_composable_value f g r h: function f -> injection g -> target g = target f -> is_left_inverse g r -> (sub (Imf f) (Imf g)) -> h = r \co f -> g \co h = f.
proof: Proof. move=> ff ig tgtf lirg hyp ->. have trsg :=(left_i_target lirg). have [crg crgi] := lirg. have srtg:=(proj33 crg). have crf: (r \coP f) by split=> //; try fct_tac; rewrite srtg. have cgrf: g \coP (r \co f) by split; try fct_tac; symmetry; aw. have cgr: (g \coP r) by split => //; fct_tac. apply: function_exten; aw; trivial;try fct_tac. move=> x xf; rewrite !compfV //; last by aw. have: (inc (Vf f x) (Imf g)) by apply: hyp;Wtac. move/(Imf_P (proj1 ig))=> [y ys ->]. by move: (f_equal (fun z=> (Vf z y)) crgi); rewrite compfV // idV // => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)