`omega` ではなくて `lia` を使うよう促すべき？

Zulip でこんなことを言っている人がいた。

Robin Arnez: Well, omega is only really meant to be used inside of lean core for bootstrapping reasons so omega is essentially frozen and won't get any such fixes. Outside of core, you're meant to use lia as the replacement. Otherwise, if you're asking why negative modulo does not work, well for some reason omega specifically checks for the right-hand side to be a natural number literal... for some reason.

see: #general > omega doesn't close modulo by negative literal @ 💬

これを信じるなら omega タクティクは非推奨であり、lia タクティクを使うべきということになる。

Start by searching the repository for references to the omega and lia tactics; the issue does not name a file or test. Confirm the current guidance from the linked Zulip discussion, then update the relevant documentation if the recommendation is verified.