proposition: Lemma unshift_but_last s : forall x, ~ In 0 (x::s) -> unshift (but_last x s) = but_last (Nat.pred x) (unshift s).
proof: Proof. induction s; cbn. - auto. - intros;f_equal. destruct x. destruct H; auto. simpl. specialize (IHs a). simpl in IHs. destruct a. destruct H; auto. simpl. simpl in IHs. f_equal. apply IHs. tauto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)