proposition: Lemma bijectiveC_pr (a b:Set) (f:a->b) (y:b): bijectiveC f -> exists! x:a, f x =y.
proof: Proof. move=> [fi fs]; apply /unique_existence; split; first by apply: fs. by move=> x x' <- veq; symmetry; apply: fi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)