proposition: Lemma rev_rev_part p : rev_part (rev_part p) = p.
proof: Proof. rewrite {2}/rev_part -{2}[p]/(catrev_part Pnil p); move: p Pnil. by elim=> //= [s h|h f1|h f1 f2|h f1 f2 f3] p IHp p'; rewrite IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)