proposition: Lemma size_mirror_part p : size_part (mirror_part p) = size_part p.
proof: Proof. rewrite /mirror_part -[RHS]addn0 -[0]/(size_part Pnil). elim: p Pnil (get_hat p) => //= [s h|h f1|h f1 f2|h f1 f2 f3] p IHp q h0; by rewrite IHp !addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)