proposition: Lemma slt_rcons x y k ks : x <[rcons ks k] y = if y \in ks then x <[ks] y else (x \in ks) || (k != y) && (k == x).
proof: Proof. rewrite /seq_lt !index_rcons. case X: (x \in ks); case Y: (y \in ks)=>//=. - by case: eqP; [rewrite index_mem | rewrite ltnS index_size]. - move/negbT/index_memN: X=>X; rewrite [LHS]ltnNge [RHS]ltnNge. rewrite X index_size /=. case: eqP=>//; first by rewrite index_size. by rewrite ltnW // ltnS index_size. rewrite !(eq_sym k). case: eqP=>_; case: eqP=>_ /=. - by rewrite ltnn. - by rewrite ltnS leqnn. - by rewrite ltnNge leqnSn. by rewrite ltnn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)