proposition: Lemma sorted_cons l r : sorted (cons l r) -> (l <=R head l r) /\ sorted r.
proof: Proof. Proof using Rrefl. by case: r => [| r0 r] //= /andP[]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)