proposition: Lemma sorted_ge_suffix : forall l1 n l2, sorted_ge n (l1 ++ l2) -> sorted_ge (simple_last n l1) l2.
proof: Proof. induction l1. - intros; cbn. assumption. - destruct l1. + cbn; inversion_clear 1; auto with lists. + inversion_clear 1; cbn in *; eauto with lists. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)