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