proposition: Lemma mirror_inv G : mirror (mirror G) =m G.
proof: Proof. case: G (@nodeI G) (@faceI G) => d e n f eK /= nI fI. apply: EqHypermap; first 1 [move=> x /=] || exact: finv_inv. by rewrite -[in LHS](eK x) !finv_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)