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