Stream: Coq users

Topic: omega

Darij Grinberg (Feb 18 2022 at 21:08):

Unable to locate library Omega. (While searching for a .vos file.)

Did it get renamed?

Laurent Théry (Feb 18 2022 at 21:15):

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.

Darij Grinberg (Feb 18 2022 at 21:17):

oof thank you!

Last updated: Sep 23 2023 at 06:01 UTC