proposition: Lemma bij_surj f: bijection f -> (forall y, inc y (target f) -> exists2 x, inc x (source f) & y = Vf f x).
proof: Proof. move => h; exact: (proj2 (proj2 h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)