proposition: Lemma canonical_decomposition f (r:= equivalence_associated f): function f -> f = (canonical_injection (Imf f) (target f)) \co (restriction2 (fun_on_quotient r f) (quotient r) (Imf f) \co (canon_proj r)).
proof: Proof. move=> ff. set (g:= canon_proj r). set (a:= Imf f). set (j:=canonical_injection a (target f)). set (k:=restriction2 (fun_on_quotient r f) (quotient r) a). have [er sr]:= (graph_ea_equivalence ff). have sat: sub a (target f) by rewrite /a ; apply: Imf_Starget. have fj:function j by rewrite /j;apply: ci_f. have foq: function (fun_on_quotient r f) by apply: foqc_f. have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) a. hnf;rewrite{2 3}/fun_on_quotient/section_canon_proj; aw;split => //. move => x /(dirim_P) [z zq zj]. rewrite (Vf_pr foq zj) foqc_V //; apply/Imf_P => //. exists (rep z) => //; rewrite - sr; fprops. move: (proj31 (restriction2_prop ra)) => fr. have fk:function k by rewrite /k. have ckg:k \coP g. by rewrite /k/g; split; fprops; rewrite /restriction2;aw. have sfg: source f = source g by rewrite /g; aw. have fkg: function (k \co g) by fct_tac. have cjkg: j \coP (k \co g). by split => //; rewrite/j/k/canonical_injection/restriction2; aw. apply: function_exten=>//; try fct_tac; aw; trivial. by rewrite/j/canonical_injection; aw. move=> x xsf. move: (xsf); rewrite - sr=> xsr; rewrite sfg in xsf. have a1: (quotient r = target g) by rewrite /g;aw. have W1q: inc (Vf g x) (quotient r) by Wtac; fct_tac. have p1: inc (Vf k (Vf g x)) a. have ->: (a = target k) by rewrite/k/restriction2; aw. by Wtac; rewrite /k/restriction2; aw;trivial; ue. rewrite compfV // ? compf_s // compfV// ci_V // restriction2_V //. rewrite foqc_V // canon_proj_V //. have : (related r x (rep (class r x))) by apply: related_rep_class. by move/(ea_relatedP ff) => [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)