proposition: Lemma fitp_cat x p1 p2 : fitp x (cat_part p1 p2) = fitp x p1 && fitp (iter (size_part p1) face x) p2.
proof: Proof. elim: p1 x => //= [s h|h f1|h f1 f2|h f1 f2 f3] p1 IHp x; by rewrite -?andbA -iterS iterSr -IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)