proposition: Lemma fcard1P (A : pred G) : fclosed face A -> reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ cface x y) (1 < fcard face A).
proof: Proof. move=> clAf; apply: (iffP idP) => [lt1fA | [x Ax [y Ay not_xFy]]]. have /card_gt0P[x /andP[/= rFx Ax]] := ltnW lt1fA; exists x => //. rewrite [fcard _ _](cardD1 x) inE /= rFx Ax ltnS in lt1fA. have /card_gt0P[y /and3P[/= neq_xy rFy Ay]] := lt1fA; exists y => //. by rewrite cfaceC (sameP (rootP cfaceC) eqP) (eqP rFx) (eqP rFy). rewrite [fcard _ _](cardD1 (froot face x)) (cardD1 (froot face y)). rewrite !inE !(roots_root cfaceC) -!(closed_connect clAf (connect_root _ _)). by rewrite Ax Ay (sameP eqP (rootP cfaceC)) cfaceC not_xFy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)