proposition: Lemma fcard_sumf : fcard sumf {:T1 + T2} = fcard f1 T1 + fcard f2 T2.
proof: Proof. pose a (x : T1 + T2) := x : bool. have ? := sumf_connect_sym; have ? := fconnect_sym inj_f1; have ? := fconnect_sym inj_f2. have ? : fclosed sumf a by move => [u|u] [v|v]. have ? : fclosed sumf (predC a) by apply: predC_closed. rewrite (n_compC a) (adjunction_n_comp _ _ _ _ adjunction_sumf_inl) //. by rewrite (adjunction_n_comp _ _ _ _ adjunction_sumf_inr). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)