proposition: Lemma update_length: forall A (L : list A) i x, length (update L i x) = length L.
proof: Proof. induction L; auto; destruct i; simpl; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset