proposition: Lemma eq_simple p q : fband p =i fband q -> size p = size q -> simple p = simple q.
proof: Proof. move=> eq_fband eq_sz; apply/eq_uniq=> [|x]; first by rewrite !size_map. apply/mapP/mapP=> [[y q_y] | [y p_y]] -> {x}. have: (y \in fband q) by rewrite -eq_fband (subsetP (ring_fband _)). by case/hasP=> z qz yFz; exists z; last by rewrite (rootP cfaceC yFz). have: (y \in fband p) by rewrite eq_fband (subsetP (ring_fband _)). by case/hasP=> [z pz yFz]; exists z; last by rewrite (rootP cfaceC yFz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)