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