proposition: Lemma scycle_cface : scycle -> {in p &, forall x y, cface x y -> x = y}.
proof: Proof. by move/scycle_simple/simple_cface. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)