proposition: Lemma sorted_rev' {A : Type}: forall (A_rel : A -> A -> Prop) (L : list A), Sorted A_rel (rev L) -> Sorted (Basics.flip A_rel) L.
proof: Proof. intros. apply sorted_rev in H. rewrite rev_involutive in H. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset