aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ROmega4.v
blob: 58ae5b8fb8c4fb3c645e8c9799cbcc612a84a3a1 (plain)
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.
*)

Require Import ZArith ROmega.
Open Scope Z.

Goal let x := 3 in x = 3.
intros.
romega.
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.
romega.
Qed.