proposition: Lemma sorted_rconsK l r : sorted (rcons r l) -> sorted r.
proof: Proof. Proof using. by case: r => [| r0 r] //=; rewrite rcons_path => /andP[]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)