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