proposition: Lemma chordless_rot r : uniq r -> chordless (rot n0 r) = chordless r.
proof: Proof. move=> Ur; rewrite /chordless (eq_subset (mem_rot n0 r)). apply: eq_subset_r => x; rewrite !inE (next_rot n0 Ur) (prev_rot n0 Ur). by apply: eq_disjoint_r => y; rewrite !inE mem_rot. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)