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