proposition: Lemma sumf_connect_sym : connect_sym (frel sumf).
proof: Proof. exact: fconnect_sym sumf_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)