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