proposition: Lemma size_rev_part p : size_part (rev_part p) = size_part p.
proof: Proof. rewrite /rev_part -[size_part p]addn0 -[0]/(size_part Pnil). elim: p Pnil => //= [s h|h f1|h f1 f2|h f1 f2 f3] p1 IHp p2; by rewrite addSnnS IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)