I am reading Software Foundation and it used tactic “omega” in a proof. But coq says “The reference omega was not found in the current environment.” There are only OmegaLemmas and PreOmega under “coq-platform\lib\coq\theories\omega”

`omega`

is deprecated in favor of the `lia`

tactic (see Omega: a (deprecated) solver for arithmetic — Coq 8.13.2 documentation).

Just do `Require Import Lia`

in order to use it.

The next SF release (coming in the next few days) will remove Omega completely.