proposition: Lemma left_composable_valueC (a b c:Set) (f:a->b)(g:a->c) s h: surjectiveC g -> (forall (x y:a), g x = g y -> f x = f y) -> is_right_inverseC g s -> h =1 f \o s -> h \o g =1 f.
proof: Proof. move=> sg hyp rish eq x /=. by rewrite eq /=; apply: hyp; rewrite -{2} (rish (g x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)