proposition: Lemma nth_error_exchange_oob: forall A (L : list A) i j k, k >= length L -> nth_error (exchange L i j) k = None.
proof: Proof. intros. apply nth_error_None. rewrite exchange_length. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset