proposition: Lemma size_rot_part n p : size_part (rot_part n p) = size_part p.
proof: Proof. by rewrite -{2}(cat_take_drop_part n p) !size_cat_part addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)