proposition: Lemma simple_last_app {A}: forall l l1 (x y:A), simple_last x (l++(y::l1)) = simple_last y l1 .
proof: Proof. induction l; cbn. - reflexivity. - intros; now rewrite IHl. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)