proposition: Lemma sorted_cut :forall l1 n x l2, sorted_ge n (l1++(x::l2)) -> simple_last n l1 <= x.
proof: Proof. induction l1. - cbn; eapply sorted_head; eauto. - cbn; intros; eapply IHl1 with l2. cbn in H; inversion_clear H; auto with lists. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)