feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty (#15944) when IsSuccArchimedean
BddAbove.exists_isGreatest_of_nonempty
IsSuccArchimedean