proposition: Lemma bijection_inverse_aux g h: bijection g -> composable g h -> g \co h = identity (source h) -> inverse_fun g = h.
proof: Proof. move => ha hb. move: (hb) => [fg fh sgth] w. have hd:= (composable_inv_f ha). have ra:=(proj31(bijective_inv_f ha)). move /(f_equal target): (w); aw; move => tgsh. have sh: (source h) = source (inverse_fun g) by aw. move/(f_equal (compose (inverse_fun g))): w. rewrite sh (compf_id_right ra) (compfA hd hb) (bij_left_inverse ha). by rewrite sgth (compf_id_left (proj31 fh)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)