proposition: Lemma fitp_drop n p x : fitp x p -> fitp (iter n face x) (drop_part n p).
proof: Proof. elim: n p x => // n IHn p x; rewrite iterSr. case: p => //= [s h|h f1|h f1 f2|h f1 f2 f3] p; by rewrite ?andbA => /andP[]; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)