proposition: Lemma dual_inv G : dual (dual G) =m G.
proof: Proof. case: G (@edgeI G) (@nodeI G) (@faceI G) => d e n f /= eK eI nI fI. by apply: EqHypermap; apply: finv_inv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)