proposition: Lemma sorted_ordered_nth_gen (i j d d' x : nat) (s: seq nat): sorted ltn s -> i < size s -> j < size s -> nth d s i < nth d' s j -> i < j.
proof: Proof. move => h hi hj hltn. case: (ltngtP i j) => // [hji|heq]. - have hgtn := sorted_ordered_nth d d' h hji hj hi. rewrite -(ltnn (nth d s i)). apply: (ltn_trans hltn). by rewrite (nth_change_default d' d hj) (nth_change_default d d' hi). by move: hltn; rewrite heq (nth_change_default d' d hj) ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor