proposition: Lemma nth_error_le {A}: forall L x (a : A), nth_error L x = Some a -> forall y, y <= x -> exists b, nth_error L y = Some b.
proof: Proof. induction L; intros. destruct x; inversion H. destruct x. assert (y = 0) by lia. subst y. inversion H. subst a0. exists a. apply H. simpl in H. specialize (IHL _ _ H). destruct y. exists a. trivial. simpl. apply IHL. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset