proposition: Lemma sle_rconsR ks x k : x <=[rcons ks k] k -> x \in rcons ks k.
proof: Proof. rewrite sle_rcons eq_refl orbF mem_rcons inE. case X: (x \in ks); first by rewrite orbT. by rewrite orbF eq_sym; case/andP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)