proposition: Lemma update_update: forall A (L : list A) i x y, update (update L i x) i y = update L i y.
proof: Proof. induction L; intros. reflexivity. destruct i. reflexivity. simpl. f_equal. apply IHL. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset