proposition: Lemma inj_image_C f: injection f -> {when eq^~ (source f) & sub^~ (source f), {morph Vfs f : a b / a -s b}}.
proof: Proof. move=> ig a b ->; move: (proj1 ig) => fg. have [_ fv _ _ aux] := (canonical_decomposition1 fg). rewrite 3! (iim_fun_r fg). have ->: source f = target (inverse_fun (restriction_to_image f)). by rewrite {1} fv; aw. by apply: iim_fun_C1 => //; apply: (bijective_inv_f (aux ig)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)