proposition: Lemma slt_sorted_ltE ltT ks x y : irreflexive ltT -> transitive ltT -> sorted ltT ks -> x \in ks -> y \in ks -> x <[ks] y = ltT x y.
proof: Proof. move=>Is T S X Y; apply/idP/idP. - by apply: slt_sorted_lt. by apply: sorted_ord_index. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)