proposition: Lemma extension_fs: surjection f -> surjection (extension f x y).
proof: Proof. move=> [_ sf]. split; first by apply:extension_f. rewrite /extension; aw => z /setU1_P; case. move=> zt; move: (sf _ zt)=> [u us wu]. by exists u; fprops; rewrite extension_Vf_in. by move =>->; exists x; fprops; rewrite extension_Vf_out. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)