proposition: Lemma sorted_tl_sorted : forall e l, is_sorted (e :: l) -> is_sorted l.
proof: Proof. intros e l S; inversion S; auto. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)