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