proposition: Lemma composable_inv_f f: bijection f -> (inverse_fun f) \coP f.
proof: Proof. move=> bf; have fif:=(bijective_inv_f bf). split; [ done | fct_tac | by aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)