Def with_top.order_iso_sum_lex_punit

feat(data/sum/order): `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` (#15370)