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