English
For every j and i ∈ Iic(j) with i not maximal, the succ of i as an element of the subtype equals the pair consisting of the succ of i.1 and a proof.
Русский
Для каждого j и i ∈ Iic(j) при условии, что i не максимален, succ i как элемент подтипа равен паре, содержащей succ i.1 и доказательство.
LaTeX
$$$\\forall {J} [\\text{PartialOrder } J] [\\text{SuccOrder } J] {j} {i : (Set.Iic j).Elem} \\(\\text{IsMax}(i) \\Rightarrow \\mathrm{Order.succ}\,i = \\langle \\mathrm{Order.succ} i.1, \\text{proof} \\rangle\\)$$$
Lean4
theorem succ_eq_of_not_isMax [SuccOrder J] {j : J} {i : Set.Iic j} (hi : ¬IsMax i) :
Order.succ i =
⟨Order.succ i.1, by
rw [← coe_succ_of_not_isMax hi]
apply Subtype.coe_prop⟩ :=
by
ext
simp only [coe_succ_of_not_isMax hi]
