proposition: Lemma head_leq_last_sorted l r : sorted (l :: r) -> (l <=R last l r).
proof: Proof. Proof using Rrefl Rtrans. elim: r l => [//=| t0 r IHr] l /= /andP[Hl {}/IHr]. exact: Rtrans Hl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)