proposition: Lemma fband_rev_ring : fband (rev_ring r) =i fband r.
proof: Proof. move=> x; apply/hasP/hasP => [] [y r_y xFy]. rewrite mem_rev_ring in r_y. exists (next r (edge y)); first by rewrite mem_next. by rewrite (same_cface xFy) -{1}[y]ee [cface _ _](next_cycle cycRr). exists (edge (prev r y)); first by rewrite mem_rev_ring ee mem_prev. by rewrite (same_cface xFy) cfaceC [cface _ _](prev_cycle cycRr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)