proposition: Lemma genus_dual : genus dual = genus G.
proof: Proof. rewrite {1}/genus /Euler_rhs /= addnCA addnC -addnA /Euler_lhs. rewrite (eq_n_comp gcomp_dual) (fcard_finv edgeI). by rewrite (fcard_finv nodeI) (fcard_finv faceI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)