proposition: Lemma sle_rcons_inE ks x y k1 k2 : (x \in ks) || (y \in ks) -> x <=[rcons ks k1] y = x <=[rcons ks k2] y.
proof: Proof. by rewrite !sle_rcons=>/orP [] ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)