basic): `a ⩿ b → b ≤ succ a` (#17940)

Commit

3 years ago

feat(order/succ_pred/basic): `a ⩿ b → b ≤ succ a` (#17940) If `a` weakly covers `b`, then `b` is at most the successor of `a`.

Author

YaelDillies

Parents