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