Commit 2025-09-17 10:12 b16bc96c
View on Github →feat(Order): no basic lemmas and some SuccOrder biUnion lemmas (#27934)
Documents that not all possible interval inclusion lemmas will be added to Basic.lean.
Also proves some biUnion results about SuccOrder.