proposition: Lemma closure_switched (G : finType) (x y : G) (f : G -> G) (inj_f : injective f) : fclosure f (pred2 x y) =i fclosure (switch x y f) (pred2 x y).
proof: Proof. wlog suff: f inj_f / {subset fclosure f (pred2 x y) <= fclosure (switch x y f) (pred2 x y)}. { move => W z; apply/idP/idP; first exact: W. move/W; rewrite (eq_fclosure switchK); apply; exact: switch_inj. } move => z /closureP -[u] /pred2P [->|->] f_z; apply/closureP. - by have [A|A] := orP (fconnect_switchV y inj_f f_z); [exists x| exists y] => //; rewrite inE eqxx. - have := (fconnect_switchV x inj_f f_z); rewrite ![fconnect (switch y x f) _ _](eq_fconnect switchC). by case/orP; [exists y| exists x] => //; rewrite inE eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)