proposition: Lemma unshift_pred : forall (s: list nat), ~ In 0 s -> unshift s = List.map Nat.pred s.
proof: Proof. induction s. - trivial. - destruct a. + destruct 1; now left. + simpl; intro; rewrite IHs; auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)