proposition: Lemma Exercise1_3a2: surjection E13_lam.
proof: Proof. split; first by apply: Exercise1_3a0. rewrite /E13_lam {1 2}/second_proj => y; aw =>/(rangeP Exercise1_3a1) [x h]. by ex_tac; rewrite second_proj_V //; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)