proposition: Lemma bij_right_inverse f: bijection f -> f \co (inverse_fun f) = identity (target f).
proof: Proof. move=> bf. have ff: function f by fct_tac. move:(bijective_inv_f bf)(composable_f_inv bf) => iff cop. apply: function_exten; aww; first by fct_tac. by move => a atf;rewrite idV // compfV//; [apply:inverse_V | aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)