proposition: Lemma slt_total ks x y : x \in ks -> [|| x == y, x <[ks] y | y <[ks] x].
proof: Proof. rewrite /seq_lt=>H; case: ltngtP; rewrite ?orbT ?orbF //. by move/index_inj=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)