proposition: Lemma Jordan_mirror : Jordan G -> Jordan mirror.
proof: Proof. move=> JordanG [] //= x /lastP[//|p z]; rewrite (finv_inv nodeI). apply: contra (JordanG (z :: rev (x :: p))) => /and3P[/andP[p'x Up]] /=. rewrite (eq_path clink_mirror) -[path _ _ _]rev_path last_rcons belast_rcons. rewrite -cons_uniq -rev_rcons rev_uniq /= p'x {}Up => -> pnzn'x /=. have{p'x} nz'x: x != node z by rewrite (memPnC p'x) ?(mem2l pnzn'x). rewrite -cats1 mem2r_cat ?inE ?(canF_eq (f_finv nodeI)) {nz'x}// in pnzn'x. case/splitP2r: p / pnzn'x => p1 p2; rewrite -cat_cons rev_cat -mem_rev. by rewrite -(mem2_last x) !rev_cons last_cat !last_rcons mem2_cat => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)