proposition: Lemma nth_error_exchange'': forall A (L : list A) i j k, i <> k -> j <> k -> nth_error (exchange L i j) k = nth_error L k.
proof: Proof. unfold exchange. intros. case_eq (nth_error L i); case_eq (nth_error L j); case_eq (nth_error L k); intros; auto; rewrite nth_error_update'; auto; rewrite nth_error_update'; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset