proposition: Lemma sle_sorted_lt ltT ks x y : transitive ltT -> sorted ltT ks -> y \in ks -> x <=[ks] y -> (x == y) || ltT x y.
proof: Proof. move=>T S Y; rewrite sle_eqVlt; last by rewrite Y orbT. by case/orP=>[->//|/(slt_sorted_lt T S Y) ->]; rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)