proposition: Lemma nth_error_Some_lt Z m a (L: list Z): nth L m = Some a -> m < length L.
proof: Proof. intros H; eapply nth_error_Some; rewrite H; discriminate. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)