proposition: Lemma fconnect_sumf_rl x y : fconnect sumf (inr x) (inl y) = false.
proof: Proof. apply/negbTE/negP => /connectP[p]. elim: p x => //= -[//|x] p IHp z /andP[_]; exact: IHp. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)