basic): `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses (#15536)

Commit

3 years ago

feat(order/succ_pred/basic): `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses (#15536)

Author

vihdzp

Parents