proposition: Corollary slt_neq x y ks : x <[ks] y -> x != y.
proof: Proof. by apply/contraL=>/eqP->; rewrite slt_irr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)