The reference omega was not found in the current environment

Using Coq
1

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”

2

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.

3

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