proposition: Theorem bijective_inv_f f: bijection f -> function (inverse_fun f).
proof: Proof. rewrite /inverse_fun; move => [fi fs]. have gf: (sgraph (graph f)) by move: fi=> [ff _]; fprops. have fgf: fgraph (inverse_graph (graph f)). split; fprops; move=> x y/igraphP [px pf]/igraphP [qx qf] peq. apply: pair_exten =>//. by rewrite -peq in qf; apply: (injective_pr3 fi pf qf). apply: function_pr=>//. rewrite igraph_range // domain_fg //; fct_tac. by rewrite (igraph_domain gf) - (ImfE (proj1 fs)) (surjective_pr0 fs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)