proposition: Lemma nth_error_exchange': forall A (L : list A) i j, i < length L -> j < length L -> nth_error (exchange L i j) j = nth_error L i.
proof: Proof. unfold exchange. intros. case_eq (nth_error L i). intros. case_eq (nth_error L j); intros. case (eq_nat_dec i j); intro. subst. rewrite update_update. rewrite nth_error_update; auto. rewrite H1 in H2. auto. rewrite nth_error_update'; auto. rewrite nth_error_update; auto. apply nth_error_None in H2. lia. intro. apply nth_error_None in H1. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset