proposition: Lemma but_last_app {A} : forall s (x:A), but_last x s ++ simple_last x s :: nil = x::s.
proof: Proof. induction s; simpl; auto. intros; simpl; now rewrite IHs. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)