Lean4
instance : SuccOrder (WithTop α)
where
succ
a :=
match a with
| ⊤ => ⊤
| Option.some a => ite (succ a = a) ⊤ (some (succ a))
le_succ
a := by
obtain - | a := a
· exact le_top
change _ ≤ ite _ _ _
split_ifs
· exact le_top
· exact coe_le_coe.2 (le_succ a)
max_of_succ_le {a}
ha := by
cases a
· exact isMax_top
dsimp only at ha
split_ifs at ha with ha'
· exact (not_top_le_coe _ ha).elim
· rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha
exact (ha' ha).elim
succ_le_of_lt {a b}
h := by
cases b
· exact le_top
cases a
· exact (not_top_lt h).elim
rw [coe_lt_coe] at h
change ite _ _ _ ≤ _
split_ifs with ha
· rw [succ_eq_iff_isMax] at ha
exact (ha.not_lt h).elim
· exact coe_le_coe.2 (succ_le_of_lt h)
