proposition: Lemma exchange_eq': forall A (L : list A) i j a, nth_error L i = a -> nth_error L j = a -> exchange L i j = L.
proof: Proof. unfold exchange. intros. rewrite H, H0. destruct a; trivial. replace (update L j a) with L. apply update_idem; trivial. symmetry. apply update_idem; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset