proposition: Lemma mirror_mirror_part p : mirror_part (mirror_part p) = p.
proof: Proof. rewrite {2}/mirror_part; move Dh0: (get_hat p) => h0. have Eh0: next_hat (if p is Pnil then Pr59 else h0) Pnil = next_hat h0 p. by rewrite -Dh0; case p. transitivity (mirror_part_rec h0 p Pnil); last by []. elim: p {Dh0}Pnil Eh0 => [|s h p IHp|h f1 p IHp|h f1 f2 p IHp|h f1 f2 f3 p IHp] q /= Eh0; by rewrite ?IHp // /mirror_part /= ?Eh0 // -Eh0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)