proposition: Theorem etp_fi f: injection f -> injection (\Pof f).
proof: Proof. move=> inf. case: (emptyset_dichot (source f))=> eq. move: inf=> [[ cf _] _]; split; fprops. rewrite {1 2} /extension_to_parts=> x y. by rewrite lf_source eq setP_0; move /set1_P => -> /set1_P ->. have [r [cfr cfri]] := (exists_left_inv_from_inj inf eq). have cfr' := (composable_for_function cfr). apply: inj_if_exists_left_inv. 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)