proposition: Lemma bijection_coq (a b: Set) (f:a->b): bijective f <-> bijectiveC f.
proof: Proof. split. move => [g ga gb]; split. by move=> x x' /(congr1 g); rewrite 2! ga. by move=> x; exists (g x). move => H; exists (inverseC H). apply: bij_left_inverseC. apply: bij_right_inverseC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)