proposition: Lemma sle_rconsI x y k ks : k != y -> x <=[ks] y -> x <=[rcons ks k] y.
proof: Proof. move=>N H; rewrite sle_rcons H N orbT andbT. case: ifP=>// K; apply: contraFT K. by rewrite negbK; apply: sle_memE H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)