proposition: Lemma nth_path_head (s : seq A) leT x0 k i : transitive leT -> i <= size s -> path leT k s -> (k == nth x0 (k::s) i) || leT k (nth x0 (k::s) i).
proof: Proof. move=>T; case: (posnP i)=>[->|N S P]; first by rewrite eqxx. apply/orP; right; elim: i N S P=>[|i] //; case: s=>//= x xs IH _. rewrite ltnS=>N /andP [H1 H2]; case: i IH N=>//= i /(_ (erefl _)) IH N. rewrite !ltnS in IH; move: (IH (ltnW N)); rewrite H1 H2=>/(_ (erefl _)). by move/T; apply; apply/pathP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)