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).
Require Import Lia in order to use it.
The next SF release (coming in the next few days) will remove Omega completely.