proposition: Lemma exchange_Permutation: forall A (L : list A) i j, Permutation (exchange L i j) L.
proof: Proof. unfold exchange. intros. case_eq (nth_error L i); auto. case_eq (nth_error L j); auto. intros. rewrite Permutation_nth_error. do 2 rewrite update_length. split; trivial. exists (fun x => if eq_nat_dec x i then j else if eq_nat_dec x j then i else x). split. do 2 intro. case (eq_nat_dec x i); case (eq_nat_dec y i); case (eq_nat_dec x j); case (eq_nat_dec y j); congruence. intro n. case (eq_nat_dec n i); intro. subst i. case (eq_nat_dec n j); intro. subst j. rewrite H in H0. inversion H0. subst a0. repeat rewrite nth_error_update; auto. rewrite update_length. apply nth_error_Some; congruence. rewrite nth_error_update'; auto. rewrite nth_error_update; auto. apply nth_error_Some; congruence. case (eq_nat_dec n j); intro. subst j. rewrite nth_error_update; auto. rewrite update_length. apply nth_error_Some; congruence. do 2 (rewrite nth_error_update'; auto). Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset