proposition: Lemma nth_leT (s : seq A) leT x0 k i : i < size s -> path leT k s -> leT (nth x0 (k::s) i) (nth x0 s i).
proof: Proof. elim: i k s=>[|i IH] k s; first by case: s=>[|x xs] //= _ /andP []. by case: s IH=>[|x xs] //= IH N /andP [P1 P2]; apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)