proposition: Lemma canonical_decomposition1C (a b:Set) (f:a->b) (g:a-> imageC f)(i:imageC f ->b): g = restriction_to_imageC f -> i = inclusionC (sub_image_targetC (f:=f)) -> [/\ injectiveC i , surjectiveC g & (injectiveC f -> bijectiveC g)].
proof: Proof. move=> gv iv. have sg: surjectiveC g. move=> x; rewrite gv. have aux: (inc (Ro x) (imageC f)) by apply: R_inc. move: (imageC_exists aux)=> [y]; exists y; apply: R_inj. by rewrite restriction_to_imageC_pr; symmetry. split => //. move=> x x' eq; move: (f_equal (@Ro b) eq). by rewrite iv 2! inclusionC_pr; apply: R_inj. move=> fi; split=> //; move=> x y eq ; move: (f_equal (@Ro (imageC f)) eq). rewrite gv 2!restriction_to_imageC_pr=> eqbis. by apply: fi; apply: R_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)