proposition: Lemma fitp_catrev x p1 p2 : fitp x (catrev_part p1 p2) = fitp x (rev_part p1) && fitp (iter (size_part p1) face x) p2.
proof: Proof. by rewrite catrev_part_eq fitp_cat size_rev_part. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)