English
The successor of x in Nat.Upto(p) exists provided that ¬p x holds; it is the element x+1 with a suitable proof that no smaller element satisfies p.
Русский
successor элемента x в Nat.Upto(p) существует при условии ¬p x; это элемент x+1 с доказательством, что ни один меньший элемент не удовлетворяет p.
LaTeX
$$$$ \\text{succ}(x,h) = \\langle x.1 + 1, \\text{proof} \\rangle \\in \\mathrm{Nat.Upto}(p). $$$$
Lean4
/-- The successor of `n` is in `Nat.Upto p` provided that `n` doesn't satisfy `p`. -/
def succ (x : Nat.Upto p) (h : ¬p x.val) : Nat.Upto p :=
⟨x.val.succ, fun j h' => by rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]⟩
