proposition: Lemma sle_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; rewrite sle_eqVlt; last by rewrite X. by rewrite (slt_sorted_leE As T S X Y); case: eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)