proposition: Theorem left_composable_value f g s h: function f -> surjection g -> source f = source g -> (forall x y, inc x (source g) -> inc y (source g) -> Vf g x = Vf g y -> Vf f x = Vf f y) -> is_right_inverse g s -> h = f \co s -> h \co g = f.
proof: Proof. move=> ff sg sfsg hyp rish ->. have sstg:= (right_i_source rish). have [cgs cgsi] := rish. have cfs: f \coP s by hnf; split; [done |fct_tac | move:cgs => [_ _] <-]. have cfsg: (f \co s) \coP g by hnf; saw;fct_tac. apply: function_exten; aw => //; first by fct_tac. move=> x xg. have Ws: (inc (Vf g x) (source s)) by rewrite sstg;Wtac;fct_tac. have WWs: inc (Vf s (Vf g x)) (source g). move:cgs => [_ _ ->]; Wtac; fct_tac. rewrite !compfV //; apply: hyp =>//; rewrite -compfV // cgsi idV //. by rewrite - sstg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)