proposition: Lemma sorted_tail : forall i j X, sorted_ge i (j::X) -> sorted_ge i X.
proof: Proof. inversion 1. - constructor. - destruct s; auto. all: inversion H4;eauto with arith lists. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)