JasonGross

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.

Lemma negb_existsb_nth_error {A} (ls : list A) (f : A -> bool) (H : existsb f ls = false) n v (H' : nth_error ls n = Some v)
  : f v = false.
Proof.
  revert dependent n; induction ls, n; cbn in *; intros; try congruence.
  all: repeat first [ progress subst
                    | rewrite orb_false_iff in *