proposition: Lemma first_proj_fs g: surjection (first_proj g).
proof: Proof. split; first by apply: first_proj_f. rewrite /first_proj /domain/Lf/Vf; aw. by move => y /funI_P [z zg ->]; ex_tac; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)