proposition: Lemma canonical_decompositiona f (r:= equivalence_associated f): function f -> function ((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 apply: Imf_Starget. have fj: function j by apply: ci_f. have ffo: 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 ffo zj) foqc_V //; apply/Imf_P => //. exists (rep z) => //; rewrite - sr; fprops. have fk:function k by rewrite /k; apply: (proj31 (restriction2_prop ra)). have ckg: k \coP g. by rewrite /k/g; split; fprops; rewrite /restriction2;aw. fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)