proposition: Lemma genus_permN : genus permN = genus G.
proof: Proof. by rewrite /genus /Euler_rhs /= addnA addnC /Euler_lhs (eq_n_comp gcomp_permN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)