proposition: Lemma predI_cface_simple x : simple -> #|[predI cface x & p]| = (x \in fband).
proof: Proof. move=> Up; case: (x \in _) / hasP => [[y py xFy] | pF'x]; last first. by apply/eq_card0=> y; apply/andP=> [[xFy py]]; case: pF'x; exists y. rewrite (cardD1 y) inE /= [y \in _]xFy py eq_card0 // => z. apply/and3P=> [[/= y'z xFz pz]]; case/eqP: y'z. by apply: simple_cface => //; rewrite -(same_cface xFz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)