proposition: Lemma unshift_shift l (H: ~ In 0 l): shift (unshift l) = l.
proof: Proof. induction l. - reflexivity. - simpl. destruct a. contradiction H; now left. simpl; rewrite IHl; auto. intro; apply H; now right. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)