proposition: Lemma canonical_decompositionb f (r:= equivalence_associated f): function f -> restriction2 (fun_on_quotient r f) (quotient r) (target f) = (fun_on_quotient r f).
proof: Proof. move=> ff. set (k:=restriction2 (fun_on_quotient r f) (quotient r) (target f)). have [er sr]:= (graph_ea_equivalence ff). have ffoq: function (fun_on_quotient r f) by apply: foqc_f. have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) (target f). hnf;rewrite{2 3}/fun_on_quotient/section_canon_proj; aw;split => //. move => x /(dirim_P) [z zq zj]. rewrite (Vf_pr ffoq zj) foqc_V //; Wtac; rewrite - sr;fprops. have fk: function k by rewrite /k; apply: (proj31(restriction2_prop ra)). have sk: source k = quotient r by rewrite /k/restriction2; aw. apply: function_exten =>//. - by rewrite /restriction2/fun_on_quotient/section_canon_proj; aw. - by rewrite/k/restriction2/fun_on_quotient; aw. - move=> x; rewrite sk => xq; rewrite restriction2_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)