proposition: Lemma right_composable_valueC (a b c:Set) (f:a->b) (g:c->b) r h: injectiveC g -> is_left_inverseC r g -> (forall u, exists v, g v = f u) -> h =1 r \o f -> g \o h =1 f.
proof: Proof. move=> ig lir hyp eq x /=; rewrite eq /=. by move: (hyp x)=> [v <-]; rewrite (left_i_v). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)