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