proposition: Lemma fconnect_sumf_l x y : fconnect sumf (inl x) (inl y) = fconnect f1 x y.
proof: Proof. by symmetry; apply: rel_functor adjunction_sumf_inl _ _ _. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)