proposition: Lemma sorted_head : forall n m s, sorted_ge n (m::s) -> n<=m.
proof: Proof. induction s. - inversion 1; auto. - inversion_clear 1. apply IHs. inversion_clear H2. + constructor; auto with arith. + constructor; eauto with arith. eapply sorted_le;eauto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)