proposition: Lemma sortedP s x : reflect (forall i, i.+1 < size s -> e (nth x s i) (nth x s i.+1)) (sorted s).
proof: Proof. by case: s => *; [constructor|apply: (iffP (pathP _ _ _)); apply]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)