proposition: Lemma but_last_shift' s : forall x, but_last (S x) (shift s) = shift (but_last x s).
proof: Proof. induction s; cbn. - auto. - intros;f_equal. rewrite IHs. cbn; reflexivity. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)