proposition: Lemma etp_inv f (g := (\Pof f)): bijection f -> bijection g /\ (inverse_fun g) = \Pof (inverse_fun f).
proof: Proof. move => bf. have bg: bijection g. split; [ exact(etp_fi (proj1 bf)) | exact(etp_fs (proj2 bf)) ]. split => //. move:(bij_right_inverse bf) => /(f_equal extension_to_parts). have ha:=(composable_for_function (composable_f_inv bf)). have hb: g \coP extension_to_parts (inverse_fun f). split; [ fct_tac | | by rewrite /g /extension_to_parts; aw]. apply:(etp_f (proj31 ha)). rewrite (etp_compose ha) etp_identity -/g => hh. apply:(bijection_inverse_aux bg) => //. by rewrite hh /extension_to_parts; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)