Commit 2024-11-23 13:41 b738c674

feat(Data/Nat/Nth): nth p n ≠ 0 lemmas (#19142) Add a few small lemmas that are convenient when working with Nat.nth, when you have a hypothesis of the form nth p n ≠ 0.

lemma lt_toFinset_card_of_nth_ne_zero {n : ℕ} (h : nth p n ≠ 0) (hf : (setOf p).Finite) :
    n < hf.toFinset.card := by

lemma nth_mem_of_ne_zero {n : ℕ} (h : nth p n ≠ 0) : p (Nat.nth p n) :=

lemma nth_ne_zero_anti (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (hb : nth p b ≠ 0) : nth p a ≠ 0 :=