proposition: Lemma nth_mono_ltn (s : seq A) ltT x0 k i j : irreflexive ltT -> transitive ltT -> i <= size s -> j <= size s -> path ltT k s -> ltT (nth x0 (k::s) i) (nth x0 (k::s) j) -> i < j.
proof: Proof. move=>I T S1 S2 P; case: ltngtP=>//; last by move=>->; rewrite I. by move/(nth_ltn_mono x0 T S2 S1 P)/T=>X /X; rewrite I. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)