proposition: Lemma Jordan_dual : Jordan G -> Jordan dual.
proof: Proof. move=> JordanG [//|x p]; apply/and3P; rewrite (eq_path clink_dual) => -[Up xCp]. rewrite /= (finv_inv faceI); move Lp: (last x p) => /= y p_fy_f'x. case/splitP2r: p / p_fy_f'x => p1 _ /splitPl[p2 p3 Lp2] in Up xCp Lp. rewrite -cat_cons !last_cat !cat_path /= Lp2 -!andbA in Lp xCp. rewrite -!cat_cons uniq_catCA catA uniq_catC in Up. case: p3 => [|z p3] in Up xCp Lp. by rewrite -Lp (f_finv faceI) /= mem_cat mem_head orbT in Up. case/and4P: xCp => xCp1 /clinkP[Lp1 | /faceI-Dy] yCp2 /=; last first. rewrite catA uniq_catC catA !cat_uniq lastI Dy in Up. by rewrite has_sym has_rcons -Lp /= mem_last andbF in Up. case/andP=> /clinkP[Dnz | Dz] zCp3; last first. by rewrite /= -Dz (f_finv faceI) -cat_cons !mem_cat mem_head !orbT in Up. have /and3P[] := JordanG (z :: p3 ++ (face y :: p2) ++ x :: p1); split=> //. rewrite cat_path /= zCp3 cat_path /= yCp2 Lp2 -Lp clinkF xCp1. by rewrite /clink /= (f_finv faceI) eqxx orbT. rewrite !last_cat /= Lp1 (finv_f nodeI) mem2_cat mem2_cons eqxx. by rewrite -cat_cons mem_cat -Dnz -Lp2 mem_last orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)