1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(** ROmega is now aware of the bodies of context variables
(of type Z or nat).
See also #148 for the corresponding improvement in Omega.
*)
From Stdlib Require Import ZArith Lia.
Open Scope Z.
Goal let x := 3 in x = 3.
intros.
lia.
Qed.
(** Example seen in #4132
(actually solvable even if b isn't known to be 5) *)
Lemma foo
(x y x' zxy zxy' z : Z)
(b := 5)
(Ry : - b <= y < b)
(Bx : x' <= b)
(H : - zxy' <= zxy)
(H' : zxy' <= x') : - b <= zxy.
Proof.
lia.
Qed.
|
