proposition: Lemma quotient_canonical_decomposition (f := fun_on_quotient s (canon_proj r)) (qr := quotient_of_relations r s): f = (fun_on_quotient qr f) \co (canon_proj qr).
proof: Proof. have sj: (surjection f) by rewrite /f;apply: foq_finer_fs. apply: (canonical_decomposition_surj2 sj). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)