Unable to locate library Omega. (While searching for a .vos file.)
Did it get renamed?
it has been replaced by the lia tactic
Require Import Lia ZArith. Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. lia. Qed.
oof thank you!
Last updated: Sep 23 2023 at 06:01 UTC