proposition: Lemma drop_nth_beyond : forall l p, length l <= p -> drop_nth l p = l.
proof: Proof. induction l; intros. destruct p; trivial. destruct p. simpl in H; lia. change (drop_nth (a::l) (S p)) with (a :: drop_nth l p). rewrite IHl; trivial. simpl in H; lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)