English
If two bounds b and b' bound a predicate P from above, and the predicate has a witness, then the numerical greatest of the two bounded greatest elements coincide.
Русский
Если два верхних границ b и b' ограничивают предикат P, и существует свидетельство существования элемента, удовлетворяющего P, то значения наибольшего элемента совпадают.
LaTeX
$$$\forall P : \mathbb{Z} \to \mathrm{Prop} \ [\mathrm{DecidablePred} \ P] \forall b \forall Hb \forall Hb' \forall Hinh, (\text{greatestOfBdd}\ b\ Hb\ Hinh).val = (\text{greatestOfBdd}\ b'\ Hb'\ Hinh).val$$$
Lean4
theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → z ≤ b)
(Hb' : ∀ z : ℤ, P z → z ≤ b') (Hinh : ∃ z : ℤ, P z) : (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh :=
by grind
