proposition: Lemma scycle_fcard_fband : scycle -> fcard face fband = size p.
proof: Proof. by move/scycle_simple/simple_fcard_fband. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)