fact: Definition exchange {A} (L : list A) (i j : nat) : list A := match nth_error L i, nth_error L j with | Some a, Some b => update (update L j a) i b | _, _ => L end.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset