proposition: Lemma sorted_rcons (s : seq A) leT (y : A) : sorted leT s -> (forall x, x \in s -> leT x y) -> sorted leT (rcons s y).
proof: Proof. elim: s=>[|a s IH] //= P H; rewrite rcons_path P /=. by apply: H (mem_last _ _). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)