proposition: Lemma exists_right_composableC (a b c:Set) (f:a->b) (g:c->b): injectiveC g -> ((exists h, g \o h =1 f) <-> (forall u, exists v, g v = f u)).
proof: Proof. move=> ig; split. by move=> [h cgh] u; exists (h u); rewrite -cgh. move => mh. case: (emptyset_dichot c) => hyp. have ae: (a = emptyset). apply /set0_P => y ya. by move: (mh (Bo ya)) => [x _]; rewrite hyp in x; case: x. symmetry in hyp; symmetry in ae. have [pa pb pc]:= empty_function_function. rewrite ae in pb; rewrite hyp in pc. exists (bcreate pa pb pc) => v. exfalso; rewrite -ae in v; case: v. have [x [xc _]]:= hyp. move: (exists_left_inv_from_injC (inhabits xc) ig) => [r rv]. exists (r \o f). move=> y /=; move: (mh y)=> [v <-]; exact (f_equal g (rv v)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)