proposition: Lemma size_cat_part p1 p2 : size_part (cat_part p1 p2) = size_part p1 + size_part p2.
proof: Proof. by apply/eqP; elim: p1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)