proposition: Lemma slt_asym x y ks : x <[ks] y -> ~~ y <[ks] x.
proof: Proof. by rewrite /seq_lt; case: ltngtP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)