proposition: Lemma sorted_behd s : sorted ord (map key s) -> sorted ord (map key (behead s)).
proof: Proof. by case: s=>//= [[??]] ?; apply: path_sorted. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)