proposition: Fact hypermap_mirrorP : @cancel3 G (face \o node) (finv node) (finv face).
proof: Proof. by move=> x; rewrite /= (finv_f faceI) (finv_f nodeI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)