proposition: Lemma canonical_decomposition1 f (g:= restriction_to_image f) (i := canonical_injection (Imf f) (target f)): function f -> [/\ i \coP g, f = i \co g, injection i, surjection g & (injection f -> bijection g )].
proof: Proof. move=> ff. move: (restriction_to_image_fs ff); rewrite -/g => sg. have Ha:sub (Imf f) (target f) by apply: Imf_Starget. have ii: injection i by apply: ci_fi. have cig: (i \coP g). by split;try fct_tac; rewrite corresp_t corresp_s ImfE. split => //. apply: function_exten=>//; aw; try fct_tac; rewrite ?corresp_s ? corresp_t //. move => x xsf. have ra:= (restriction_to_image_axioms ff). have xsg: inc x (source g) by rewrite corresp_s. rewrite compfV // restriction2_V // ci_V //; Wtac. apply: restriction_to_image_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)