proposition: Lemma exists_right_composable_uniqueC (a b c:Set)(f:a->b) (g:c->b) h h': injectiveC g -> g \o h =1 f -> g \o h' =1 f -> h =1 h'.
proof: Proof. move=> ig c1 c2 x; apply: ig; by move: (c1 x)(c2 x) => /= -> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)