proposition: Lemma exchange_update : forall A k j x y (L : list A), k < length L -> j < length L -> nth_error L k = Some x -> nth_error L j = Some y -> update (update L j x) k y = exchange L j k.
proof: Proof. intros. apply nth_error_eq. intros. case (eq_nat_dec k i); intro. subst k. rewrite nth_error_exchange'; auto. rewrite nth_error_update; auto. rewrite update_length; auto. rewrite nth_error_update'; auto. case (eq_nat_dec j i); intro. subst j. rewrite nth_error_exchange; auto. rewrite nth_error_update; auto. rewrite nth_error_exchange''; auto. rewrite nth_error_update'; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset