proposition: Lemma sorted_ge_prefix : forall l1 n l2, sorted_ge n (l1 ++ l2) -> sorted_ge n l1.
proof: Proof. induction l1. - constructor. - destruct l1. constructor. cbn in H. eapply sorted_head; eauto. constructor. cbn in H. eapply sorted_head; eauto. inversion_clear H. auto. eapply IHl1. inversion_clear H. eauto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)