proposition: Lemma unshift_not_nil : forall s, ~ In 0 s -> s <> nil -> unshift s <> nil.
proof: Proof. destruct s. - destruct 2; auto. - cbn. destruct n. + destruct 1; now left. + discriminate. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)