proposition: Lemma genus_mirror : genus mirror = genus G.
proof: Proof. rewrite [LHS]/genus /Euler_rhs /Euler_lhs (eq_n_comp gcomp_mirror). suffices <-: fcard edge G = fcard edge mirror. by rewrite (eq_n_comp cnode_mirror) (eq_n_comp cface_mirror). have:= adjunction_n_comp _ cedgeC (@cedgeC dual) _ mirror_edge_adj. by move->; first apply/esym/eq_n_comp/(same_fconnect_finv (@edgeI G)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)