proposition: Lemma has_fband_sym p1 p2 : has (mem (fband p1)) p2 = has (mem (fband p2)) p1.
proof: Proof. apply/hasP/hasP=> [] [x px /hasP[y py xFy]]; by exists y => //; apply/hasP; exists x; rewrite // cfaceC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)