proposition: Lemma inverse_bij_bp g E E': (bijection_prop g E E') -> bijection_prop (inverse_fun g) E' E.
proof: Proof. by move => [pa pb pc];hnf; aw; split => //; apply: inverse_bij_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)