proposition: Lemma eqm_genus : genus G = genus G'.
proof: Proof. rewrite {2}/genus /Euler_lhs -eqm_gcomp; have [e n f Eenf Ee En Ef] := eqGG'. by rewrite /Euler_rhs /= -(eq_fcard Ee) -(eq_fcard En) -(eq_fcard Ef). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)