proposition: Lemma exists_right_composable_auxC (a b c:Set) (f:a->b) (g:c->b) h r: is_left_inverseC g r -> g \o h =1 f -> h =1 r \o f.
proof: Proof. move=> li eq x /=; rewrite -(eq x); symmetry;exact: (li (h x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)