Commit 2026-08-12 20:03 5658ee5a

refactor: split Data.ENat.Basic (#42271) There's various assert_not_exists scattered throughout the library that don't even permit MonoidWithZero. This is causing problems on #40901, since the smallInductiveDimension of a topological space (a relatively basic notion) is WithBot ℕ∞-valued. We split Data.ENat.Basic into three files:

• Data.ENat.Basic now imports nothing about monoids.
• Data.ENat.Monoid contains the lemmas about the LinearOrderedAddCommMonoidWithTop structure.
• Data.ENat.SuccOrder contains the lemmas about the SuccAddOrder structure. No new results are added. A few proofs are tweaked slightly so as to decrease imports.