proposition: Lemma exists_left_composable_auxC (a b c:Set) (f:a->b) (g:a-> c) s h: is_right_inverseC g s -> h \o g =1 f -> h =1 f \o s.
proof: Proof. by move=> ri eq x /=; rewrite -eq /=; move: (ri x) => /= ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)