proposition: Lemma canonical_decomposition_surj2 f (r:= equivalence_associated f): surjection f -> f = (fun_on_quotient r f) \co (canon_proj r).
proof: Proof. move=> sf; move: (canonical_decomposition_surj sf). by move: sf => [ff _]; move: (canonical_decompositionb ff) => /= -> <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)