proposition: Lemma cat_take_drop_part n p : cat_part (take_part n p) (drop_part n p) = p.
proof: Proof. by elim: n p => [|n IHn] [] //= *; rewrite IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)