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