proposition: Lemma extension_fb f x y: ~ inc x (source f) -> ~ inc y (target f) -> bijection f -> bijection (extension f x y).
proof: Proof. move => ha hb [[ff injf] bf]; split; last by apply:extension_fs. split; first by apply: extension_f. rewrite {1}/extension; aw => a b /setU1_P; case => av; move/setU1_P; case => bv. - rewrite (extension_Vf_in y ff ha av) (extension_Vf_in y ff ha bv). by apply: injf. - rewrite bv (extension_Vf_in y ff ha av) (extension_Vf_out y ff ha). move => bad; case:hb; rewrite - bad; Wtac. - rewrite av (extension_Vf_in y ff ha bv) (extension_Vf_out y ff ha). move => bad; case:hb; rewrite bad; Wtac. - by rewrite av bv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)