proposition: Lemma sle_antisym ks : {in ks, antisymmetric (seq_le ks)}.
proof: Proof. rewrite /seq_le=>x Hx y. by rewrite -eqn_leq =>/eqP /index_inj; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)