English
If a ≤ b and p(nth p b) holds, then p(nth p a) also holds.
Русский
Если a ≤ b и p(nth p b) справедливо, то p(nth p a) тоже верно.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {a b}:\\\\mathbb{N},\\\\ a\\\\le b \\\\Rightarrow \\\\exists h: p\\\\(\\\\mathrm{nth}\\\\ p\\\\ b) \\\\Rightarrow \\\\ p\\\\(\\\\mathrm{nth}\\\\ p\\\\ a).$$$
Lean4
theorem nth_mem_anti {a b : ℕ} (hab : a ≤ b) (h : p (nth p b)) : p (nth p a) :=
by
by_cases h' : ∀ hf : (setOf p).Finite, a < #hf.toFinset
· exact nth_mem a h'
· simp only [not_forall, not_lt] at h'
have h'b : ∃ hf : (setOf p).Finite, #hf.toFinset ≤ b :=
by
rcases h' with ⟨hf, ha⟩
exact ⟨hf, ha.trans hab⟩
have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']
have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]
rw [ha0]
rwa [hb0] at h
