Commit 2026-03-10 20:56 1d9dd828

feat(ENat): relate addition with strict inequality (#36454) We have these theorems for WithTop and for ENNReal, but not for ENat. None of these follow from general typeclass facts, eg add_lt_add requires strict monotonicity of addition, which fails in ENat. It's worth having these explicitly, since they're already there for ENNReal, and to avoid defeq abuse around ENat/WithTop.