proposition: Lemma slt_rconsR ks x k : x <[rcons ks k] k -> x \in ks.
proof: Proof. by rewrite slt_rcons eq_refl orbF; case: ifP=>[_ /slt_memE|]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)