proposition: Lemma inverse_fun_involutiveC (a b:Set) (f:a->b) (H: bijectiveC f): f =1 inverseC(bijective_inverseC H).
proof: Proof. move=> x;move: (bijective_inverseC H) => [i s]; apply: (i). by rewrite inverseC_pra inverseC_prb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)