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