proposition: Lemma rot_scycle e p : scycle e (rot n0 p) = scycle e p.
proof: Proof. by rewrite /scycle rot_cycle simple_rot. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)