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