proposition: Lemma index_sorted (s : seq A) (leT : rel A) : uniq s -> (forall a b, a \in s -> b \in s -> index a s < index b s -> leT a b) -> sorted leT s.
proof: Proof. elim: s=>[|x xs IH] //= U H; have P : all (leT x) xs. - apply/allP=>z Z; apply: H; rewrite ?(inE,eqxx,Z,orbT) //. by case: ifP U=>// /eqP ->; rewrite Z. rewrite (path_min_sorted P); apply: IH=>[|a b Xa Xb N]; first by case/andP: U. apply: H; rewrite ?(inE,Xa,Xb,orbT) //. by case: eqP U=>[->|]; case: eqP=>[->|]; rewrite ?(Xa,Xb). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)