proposition: Lemma sorted_not_in_tail : forall i j X, Sorted lt (i::X) -> j<=i -> ~ (In j X).
proof: Proof. intros. red; intro. specialize (sorted_In _ _ H j H1). intro; abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)