proposition: Lemma fresh_bij (T : finType) (E : {fset nat}) (f : bij T E) e (He : e \notin E) : bij (option T) (e |` E).
proof: Proof. pose g (x : option T) : e |` E := if x is Some z then Sub (val (f z)) (fset1Ur (valP (f z))) else Sub e fset1U1. pose g_inv (x : e |` E) : option T := match fsetULVR (valP x) with inl _ => None | inr p => Some (f^-1 (Sub (val x) p)) end. have can_g : cancel g g_inv. { move => [x|]; rewrite /g/g_inv/=; case: (fsetULVR _) => [|p] //=. - by rewrite inE fsval_eqF. - by rewrite valK' bijK. - exfalso. by rewrite p in He. } have can_g_inv : cancel g_inv g. { move => [x Hx]; rewrite /g/g_inv/=. case: (fsetULVR _) => [|p] //=. - rewrite !inE => A. apply: val_inj => /=. by rewrite (eqP A). - apply: val_inj => //=. by rewrite bijK'. } apply: (Bij can_g can_g_inv). Defined.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)