proposition: Lemma nontrivial1P r : reflect ((exists2 x, x \in diskF r & exists2 y, y \in diskF r & ~~ cface x y) /\ (exists2 x, x \in diskFC r & exists2 y, y \in diskFC r & ~~ cface x y)) (nontrivial_ring 1 r).
proof: Proof. rewrite /nontrivial_ring. have [nzFr|] := fcard1P (diskF_face r); last by right; case. by apply: (iffP (fcard1P (diskFC_face r))) => [|[]]. 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)