proposition: Lemma order_mirror_edge (x : G) : @order mirror edge x = order edge (node x).
proof: Proof. have [_ De'] := mirror_edge_adj. apply: etrans (card_image faceI _); apply: eq_card => y. rewrite [y \in _]cedge1 {2}/edge {4}/mirror /= -(@nodeK G y) (mem_image faceI). by rewrite -topredE /= -De' // (same_fconnect_finv edgeI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)