proposition: Theorem inv_function_fb f: function f -> function (inverse_fun f) -> bijection f.
proof: Proof. move=> ff fif. split. apply: injective_pr_bis=> // x x' y. move/igraph_pP;rewrite -ifun_g => r1 ;move/igraph_pP; rewrite -ifun_g=> r2. by apply: (fgraph_pr (proj32 fif) r1 r2). apply: surjective_pr1=> //; rewrite (ImfE ff) - igraph_domain; fprops. by rewrite -ifun_g domain_fg //; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)