Lean4
instance : PredOrder (WithBot α)
where
pred
a :=
match a with
| ⊥ => ⊥
| Option.some a => ite (pred a = a) ⊥ (some (pred a))
pred_le
a := by
obtain - | a := a
· exact bot_le
change ite _ _ _ ≤ _
split_ifs
· exact bot_le
· exact coe_le_coe.2 (pred_le a)
min_of_le_pred {a}
ha := by
cases a with
| bot => exact isMin_bot
| coe a =>
dsimp only at ha
split_ifs at ha with ha'
· exact (not_coe_le_bot _ ha).elim
· rw [coe_le_coe, le_pred_iff_isMin, ← pred_eq_iff_isMin] at ha
exact (ha' ha).elim
le_pred_of_lt {a b}
h := by
cases a
· exact bot_le
cases b
· exact (not_lt_bot h).elim
rw [coe_lt_coe] at h
change _ ≤ ite _ _ _
split_ifs with hb
· rw [pred_eq_iff_isMin] at hb
exact (hb.not_lt h).elim
· exact coe_le_coe.2 (le_pred_of_lt h)
