proposition: Lemma inverse_bij_fb f: bijection f -> bijection (inverse_fun f).
proof: Proof. move=> bf;move: (bijective_inv_f bf)=> bif. have ff:function f by fct_tac. apply: inv_function_fb => //; rewrite ifun_involutive //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)