proposition: Lemma slt_sorted_leE leT ks x y : antisymmetric leT -> transitive leT -> sorted leT ks -> x \in ks -> y \in ks -> x <[ks] y = (x != y) && leT x y.
proof: Proof. move=>As T S X Y; apply/idP/idP. - by case: eqP=>[->|/eqP N] /=; [apply: contraLR; rewrite slt_irr | apply: slt_sorted_lt]. by case/andP=>H K; apply: sorted_ord_index_leq K H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)