proposition: Lemma bijective_inverseC: bijectiveC (inverseC H).
proof: Proof. split. by move=> x y sv; rewrite -(inverseC_prb x) -(inverseC_prb y) sv. by move=> u; exists (f u); rewrite inverseC_pra. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)