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