proposition: Lemma canonical_decomposition_surj f (r:= equivalence_associated f): surjection f -> f = (restriction2 (fun_on_quotient r f) (quotient r) (target f)) \co (canon_proj r).
proof: Proof. move=> sf. move: (surjective_pr7 sf) (surjective_pr0 sf) => p1 p2. move: sf => [sf _]. move: (canonical_decomposition sf); rewrite /= p1 p2 -/r => {1} ->. set (g:= (restriction2 (fun_on_quotient r f) (quotient r) (target f))). set (h:= g \co (canon_proj r)). have fh: function h by move:(canonical_decompositiona sf); rewrite -/r p2. have -> : (target f = target h) by rewrite /h/g/restriction2; aw. by apply:compf_id_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)