proposition: Lemma sorted_ordered_nth i j d d' (s: seq nat): sorted ltn s -> i < j -> i < size s -> j < size s -> nth d s i < nth d' s j.
proof: Proof. case: s => [ | hd tl] //= /path_ordered_nth => h h1 h2 h3. by apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor