proposition: Lemma insertE_rot p : insertE (rot n0 p) = rot (double n0) (insertE p).
proof: Proof. have [p_ge_n0 | p_lt_n0] := leqP (size p) n0. by rewrite !rot_oversize // size_insertE leq_double. rewrite -{2}(cat_take_drop n0 p) {1}/rot !insertE_cat -rot_size_cat. by rewrite size_insertE (size_takel (ltnW _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)