proposition: Lemma exchange_eq: forall A (L : list A) i, exchange L i i = L.
proof: Proof. unfold exchange. intros. case_eq (nth_error L i); auto. intros. rewrite update_update. rewrite update_idem; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset