proposition: Lemma fcard_switch x y (xDy : x != y) : fcard (switch x y f) G = if fconnect f x y then (fcard f G).+1 else (fcard f G).-1.
proof: Proof. pose xswitch := switch x y f. have f_sym := fconnect_sym inj_f; have sw_sym := fconnect_sym (@switch_inj _ x y _ inj_f). pose a := fclosure f (pred2 x y). have cCa : fclosed f [predC a] by apply/predC_closed/closure_closed. have eq_ab : a =i fclosure xswitch (pred2 x y) by apply: closure_switched. rewrite (n_compC a) (eq_n_comp_r eq_ab) (n_comp_closure2 sw_sym). rewrite (n_compC a) (n_comp_closure2 f_sym). have adj_f: fun_adjunction id f xswitch (predC a). { apply: strict_adjunction => //. - by apply/subsetP => z _; rewrite -[z]/(id z) codom_f. - move => u v H. apply: switch_base. apply: contraNN H. rewrite [in X in _ -> X]/= negbK; exact: mem_closure. } rewrite fconnect_switched // negbK (adjunction_n_comp _ f_sym sw_sym _ adj_f) //. rewrite !(eq_n_comp_r (_ : _ =i [predC a])) //. by case: (fconnect f x y); rewrite /= ?add2n ?add1n. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)