proposition: Fact hypermap_dualP : @cancel3 G (finv edge) (finv face) (finv node).
proof: Proof. by move=> x; rewrite -{1}[x]faceK (finv_f edgeI) (finv_f nodeI) (finv_f faceI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)