proposition: Lemma gpath_uniq t1 t2 p : gpath t1 t2 p -> uniq (t1 :: p).
proof: Proof. move=> gH; apply/(uniqP t1) => i j iH jH. wlog : i j iH jH / i <= j. move=> H; case: (leqP i j) => [iLj|jLi]; first by apply: H. by move=> /(@sym_equal _ _ _) /H->; rewrite // ltnW. rewrite leq_eqVlt => /orP[/eqP->//|iLj]. case/gpathP : gH => t1Pp t1pLt2 dt1t2E. case: j jH iLj => j // jH iLj. case: i iH iLj => [_ _ t1E | ] //. pose p1 := drop j.+1 p. have t1Pp1 : path r t1 p1. move: (t1Pp); rewrite -[p](cat_take_drop j.+1) cat_path. rewrite /= in t1E. by rewrite (last_take t1) //= -t1E => /andP[]. have t1p1L : last t1 p1 = t2. move: (t1pLt2); rewrite -[p](cat_take_drop j.+1) last_cat. rewrite /= in t1E. by rewrite (last_take t1) //= -t1E. have [] := boolP (`d[t1, t2] <= size p1) => [|/negP[]]; last first. by apply: gdist_path_le. rewrite leqNgt => /negP[]. rewrite size_drop dt1t2E. rewrite /= in t1E. by rewrite -{2}[size p](subnK (_ : j < size p)) // addnS ltnS leq_addr. move=> i iH; rewrite ltnS => iLj nE. pose p1 := take i.+1 p ++ drop j.+1 p. have [] := boolP (`d[t1, t2] <= size p1) => [|/negP[]]. rewrite leqNgt => /negP[]. rewrite size_cat size_take size_drop ifT //; last first. by rewrite -ltnS in iLj; apply: leq_trans iLj _. rewrite dt1t2E -{2}[size p](subnK (_ : j < size _)) //. by rewrite addnC ltn_add2l. apply: gdist_path_le. move: t1Pp; rewrite -[p](cat_take_drop i.+1). rewrite -[drop _ _](cat_take_drop (j - i)) !cat_path. case/and3P => [-> _] /=. rewrite !(last_take t1) /=; last first. - rewrite size_drop -subSS. by apply: leq_sub2r. - by apply: leq_trans iLj _; rewrite ltnW //. rewrite drop_drop addnS subnK; last by rewrite ltnW. congr path. move: (nE) => /= ->. rewrite -[j - i]prednK //. by rewrite /= nth_drop -subnS addnC subnK //. by rewrite subn_gt0. rewrite last_cat (last_take t1) // nE. by rewrite -t1pLt2 -{3}[p](cat_take_drop j.+1) last_cat (last_take t1). Qed.
imports: mathcomp(all_ssreflect)