proposition: Lemma size_split_part i j k lo p : size_part (split_part i j k lo p) = size_part p.
proof: Proof. move: (size_rot_part j p); rewrite /rot_part size_cat_part addnC. case: i => //=; case: (drop_part j p) => [|s h|h f1|h f1 f2|h f1 f2 f3] //= p'; by try case: s; rewrite //= ?size_cat_part. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)