proposition: Lemma simplify_rlink x p : path rlink x p -> exists2 p', path rlink x p' /\ simple p' & [/\ last x p = last x p', nilp p = nilp p' & all [mem p] p'].
proof: Proof. elim: {p}_.+1 x {-2}p (ltnSn (size p)) => // n IHn x. case=> [|y p]; [by exists [::] | rewrite /= ltnS] => lt_p_n /andP[xRy yRp]. case pFy: (y \in fband p); last first. have{n IHn lt_p_n yRp} [q [xRq Uq] [Lq _ /allP/= sqp]] := IHn y p lt_p_n yRp. exists (y :: q); split; rewrite /= ?xRy ?mem_head //=. rewrite simple_cons (contraFN _ pFy) // => /hasP[z /sqp qz yFz]. by apply/hasP; exists z. by apply/allP=> z qz; rewrite !inE sqp ?orbT. case/fprojP: pFy; move: (fproj p y) => z pz yFz. case/splitPr: pz yRp lt_p_n => p1 p2; rewrite cat_path /= => /and3P[_ _ zRp2]. rewrite last_cat /= size_cat => /(leq_ltn_trans (leq_addl _ _)) lt_p2_n. have{zRp2} xRp2: path rlink x (z :: p2) by rewrite /= -(rlinkFr yFz) xRy. have{n IHn lt_p2_n} [q [xRq Uq] [Lq ntq /allP/= sqp2]] := IHn x _ lt_p2_n xRp2. by exists q; split=> //; apply/allP=> t qt; rewrite !inE mem_cat sqp2 ?orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)