English
If a < nth p (k+1) and p a, then a ≤ nth p k.
Русский
Если a < nth p (k+1) и p a, тогда a ≤ nth p k.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {k a}:\\\\mathbb{N},\\\\ a <\\\\ nth\\\\ p\\\\ (k+1) \\\\Rightarrow \\\\ p a \\\\Rightarrow a \\\\le \\\\mathrm{nth}\\\\ p\\\\ k.$$$
Lean4
theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a ≤ nth p k :=
by
rcases (setOf p).finite_or_infinite with hf | hf
· rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk
·
rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff, ←
(nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
· rw [nth_of_card_le _ hk] at h
exact absurd h (zero_le _).not_gt
· rcases subset_range_nth ha with ⟨n, rfl⟩
rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h
