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