proposition: Lemma lt_sorted_uniq_le (s : seq A) ltT : irreflexive ltT -> antisymmetric ltT -> transitive ltT -> sorted ltT s = uniq s && (sorted (fun k t => (k == t) || ltT k t) s).
proof: Proof. move=>I As T; case: s=>// n s; elim: s n=>//= m s IHs n. rewrite inE negb_or IHs -!andbA /=. case: (n =P m)=>[->|/eqP Nm /=]; first by rewrite I. case lTnm : (ltT n m)=>/=; last by rewrite !andbF. case Ns: (n \in s)=>//=; do !bool_congr. have T' : transitive (fun k t => (k == t) || ltT k t). - move=>x y z /orP [/eqP -> //|H]. case/orP=>[/eqP <-|]; first by rewrite H orbT. by move/(T _ _ _ H)=>->; rewrite orbT. apply/negP=>/(order_path_min T')/allP/(_ n Ns). rewrite eq_sym (negbTE Nm) /= =>lTmn. by rewrite (As m n) ?eqxx // lTnm lTmn in Nm. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)