proposition: Lemma simple_fcard_fband : simple -> fcard face fband = size p.
proof: Proof. move=> Up; rewrite -(size_map (froot face) p) -(card_uniqP Up). apply/eq_card=> x; apply/andP/mapP=> [[rFx /hasP[y py xFy]] | [y py ->]]. by exists y; rewrite // -(rootP cfaceC xFy) (eqP rFx). split; first exact: (roots_root cfaceC y). by apply/hasP; exists y; last by rewrite cfaceC connect_root. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)