proposition: Lemma nth_ltn_mono (s : seq A) leT x0 k i j : transitive leT -> i <= size s -> j <= size s -> path leT k s -> i < j -> leT (nth x0 (k::s) i) (nth x0 (k::s) j).
proof: Proof. move=>T S1 S2 P; elim: j S2=>[|j IH] //= S2. move: (nth_leT x0 S2 P)=>L. rewrite ltnS leq_eqVlt=>/orP; case=>[/eqP -> //|]. by move/(IH (ltnW S2))/T; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)