proposition: Lemma double_dart (x y : G) : cface x y -> cface (edge x) (edge y) -> x = y.
proof: Proof. move=> xFy exFey; apply: contraTeq isT => y'x /=. have Ur: scycle rlink [:: x; edge y] by rewrite srcycleI //= exFey ee cfaceC. by rewrite -(Birkhoff _ Ur) // nontrivial_cycle2 // (inj_eq edgeI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)