proposition: Lemma existsb_nth : forall l n d, n < length l -> existsb l = false -> f (nth n l d) = false.
proof: Proof. intro l; induction l as [|a ? IHl]; [easy|]. cbn. intros [|n]; [now destruct (f a)|]. intros d ? %Nat.succ_lt_mono. now destruct (f a); [|apply IHl]. Qed.
imports: PeanoNat