English
If n > 0 and i > 0, then p.succAbove i > 0 for any p ∈ Fin(n+1).
Русский
Если n > 0 и i > 0, то p.succAbove i > 0 для любого p ∈ Fin(n+1).
LaTeX
$$$\forall n \in \mathbb{N}\, [\mathrm{NeZero}\ n] \rightarrow \forall p \in \mathrm{Fin}(n+1)\, \forall i \in \mathrm{Fin}(n),\ 0 < i \Rightarrow 0 < p.succAbove(i).$$$
Lean4
/-- Embedding a positive `Fin n` results in a positive `Fin (n + 1)` -/
theorem succAbove_pos [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) : 0 < p.succAbove i :=
by
by_cases H : castSucc i < p
· simpa [succAbove_of_castSucc_lt _ _ H] using castSucc_pos' h
· simp [succAbove_of_le_castSucc _ _ (Fin.not_lt.1 H)]
