proposition: Lemma path_ordered_nth (i j d d' x : nat) (s: seq nat): path ltn x s -> i < j -> i < size (x::s) -> j < size (x::s) -> nth d (x::s) i < nth d' (x::s) j.
proof: Proof. move => hp hij h1 h2. have hin : nth d' (x :: s) j \in (drop i.+1 (x :: s)). - move=> {hp}/=. elim : s x d' i j hij h1 h2 => [ | hd tl hi] x d' [ | i] [ | j] hij //=. + rewrite -[j.+1]add1n -[(size tl).+1]add1n ltn_add2l => _ h. by rewrite mem_nth. rewrite -[i.+1]add1n -[(size tl).+1]add1n -[j.+1]add1n !ltn_add2l => h1 h2. by apply: hi. move/(order_path_min trans_ltn)/allP: (path_drop d hp hij)=> h. by apply: (h _ hin). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor