proposition: Theorem etp_fs f: surjection f -> surjection (\Pof f).
proof: Proof. move=> sf; apply: surj_if_exists_right_inv. have [r [cfr cfri]]:= (exists_right_inv_from_surj sf). have cfr' := (composable_for_function cfr). exists (extension_to_parts r); split; first by apply: etp_composable. by rewrite - etp_compose // cfri etp_identity /extension_to_parts; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)