proposition: Lemma exchange_length: forall A (L : list A) i j, length (exchange L i j) = length L.
proof: Proof. unfold exchange. intros. case nth_error; trivial. case nth_error; trivial. intros. do 2 rewrite update_length. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset