proposition: Lemma closed_sumf_l : fclosed sumf is_inl.
proof: Proof. by move => [u|u] [v|v]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)