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