Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

7 files changed, 619 insertions, 0 deletions

diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v
new file mode 100644
index 00000000..6951fcd3
--- /dev/null
+++ b/test-suite/micromega/bertot.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import ZArith.
+Require Import Micromegatac.
+
+Open Scope Z_scope.
+
+Goal (forall x y n,
+  ( ~ x < n /\ x <= n /\ 2 * y = x*(x+1) -> 2 * y = n*(n+1))
+  /\
+  (x < n /\ x <= n /\ 2 * y = x * (x+1) -> x + 1 <= n /\ 2 *(x+1+y) = (x+1)*(x+2))).
+Proof.
+  intros.
+  micromega Z.
+Qed.
+
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
new file mode 100644
index 00000000..dc78ace5
--- /dev/null
+++ b/test-suite/micromega/example.v
@@ -0,0 +1,347 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import ZArith.
+Require Import Micromegatac.
+Require Import Ring_normalize.
+Open Scope Z_scope.
+Require Import ZMicromega.
+Require Import VarMap.
+
+(* false in Q : x=1/2 and n=1 *)
+
+Lemma not_so_easy : forall x n : Z,
+  2*x + 1 <= 2 *n -> x <= n-1.
+Proof.
+  intros.
+  zfarkas. 
+Qed.
+
+
+(* From Laurent Théry *)
+
+Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Proof.
+  intros. 
+  micromega Z. 
+Qed.
+
+
+Lemma Zdiscr: forall a b c x, 
+  a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+
+Lemma plus_minus : forall x y, 
+  0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
+Proof.
+  intros.
+  zfarkas.
+Qed.
+
+
+
+Lemma mplus_minus : forall x y, 
+  x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma pol3: forall x y, 0 <= x + y ->  
+  x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+
+(* Motivating example from: Expressiveness + Automation + Soundness: 
+   Towards COmbining SMT Solvers and Interactive Proof Assistants *)
+Parameter rho : Z.
+Parameter rho_ge : rho >= 0.
+Parameter correct : Z -> Z -> Prop.
+
+
+Definition rbound1 (C:Z -> Z -> Z) : Prop :=
+  forall p s t, correct p t /\ s <= t -> C p t - C p s <= (1-rho)*(t-s).
+
+Definition rbound2 (C:Z -> Z -> Z) : Prop :=
+  forall p s t, correct p t /\ s <= t ->  (1-rho)*(t-s) <= C p t - C p s.
+
+
+Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t  /\ correct q t /\
+  rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  -> 
+  Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s).
+Proof.
+  intros.
+  generalize (Zabs_eq (C p t - D q t)).
+  generalize (Zabs_non_eq (C p t - D q t)).
+  generalize (Zabs_eq (C p s -D q s)).
+  generalize (Zabs_non_eq (C p s - D q s)).
+  unfold rbound2 in H.
+  unfold rbound1 in H.
+  intuition.
+  generalize (H6 _ _ _ (conj H H4)).
+  generalize (H7 _ _ _ (conj H H4)).
+  generalize (H8 _ _ _ (conj H H4)).
+  generalize (H10 _ _ _ (conj H H4)).
+  generalize (H6 _ _ _ (conj H5 H4)).
+  generalize (H7 _ _ _ (conj H5 H4)).
+  generalize (H8 _ _ _ (conj H5 H4)).
+  generalize (H10 _ _ _ (conj H5 H4)).
+  generalize rho_ge.
+  micromega Z.
+Qed.
+
+(* Rule of signs *)
+
+Lemma sign_pos_pos: forall x y,
+  x > 0 -> y > 0 -> x*y > 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_pos_zero: forall x y,
+  x > 0 -> y = 0 -> x*y = 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_pos_neg: forall x y,
+  x > 0 -> y < 0 -> x*y < 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_zer_pos: forall x y,
+  x = 0 -> y > 0 -> x*y = 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_zero_zero: forall x y,
+  x = 0 -> y = 0 -> x*y = 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_zero_neg: forall x y,
+  x = 0 -> y < 0 -> x*y = 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_neg_pos: forall x y,
+  x < 0 -> y > 0 -> x*y < 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_neg_zero: forall x y,
+  x < 0 -> y = 0 -> x*y = 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+Lemma sign_neg_neg: forall x y,
+  x < 0 -> y < 0 -> x*y > 0.
+Proof.
+  intros; micromega Z.
+Qed.
+
+
+(* Other (simple) examples *)
+
+Lemma binomial : forall x y, (x+y)^2 = x^2 + 2*x*y + y^2.
+Proof.
+  intros.
+  zfarkas.
+Qed.
+
+Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
+Proof.
+  intros.
+  micromega Z.
+Qed.
+
+
+Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
+Proof.
+  intros.
+  micromega Z.
+Qed.
+
+
+Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 ->  False.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+(* Found in Parrilo's talk *)
+(* BUG?: certificate with **very** big coefficients *)
+Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
+Proof.
+  intros.
+  micromega Z.
+Qed.
+
+
+(* from hol_light/Examples/sos.ml *)
+
+Lemma hol_light1 : forall a1 a2 b1 b2,
+  a1 >= 0 -> a2 >= 0 -> 
+   (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> 
+   (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+
+Lemma hol_light2 : forall x a,
+        3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
+Proof.
+ intros ; micromega Z.
+Qed.
+
+Lemma hol_light3 : forall b a c x,
+  b ^ 2 < 4 * a * c -> (a * x ^2  + b * x + c = 0) -> False.
+Proof.
+intros ; micromega Z.
+Qed.
+
+Lemma hol_light4 : forall a c b x,
+  a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
+Proof.
+intros ; micromega Z.
+Qed.
+
+Lemma hol_light5 : forall x y,
+    0 <= x /\ x <= 1 /\ 0 <= y /\ y <= 1
+     -> x ^ 2 + y ^ 2 < 1 \/
+      (x - 1) ^ 2 + y ^ 2 < 1 \/
+      x ^ 2 + (y - 1) ^ 2 < 1 \/
+      (x - 1) ^ 2 + (y - 1) ^ 2 < 1.
+Proof.
+intros; micromega Z.
+Qed.
+
+
+
+Lemma hol_light7 : forall x y z,
+ 0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
+  -> x * y + x * z + y * z >= 3 * x * y * z.
+Proof.
+intros ; micromega Z.
+Qed.
+
+Lemma hol_light8 : forall x y z,
+ x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+Lemma hol_light9 : forall w x y z,
+ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
+  -> (w + x + y + z) ^ 2 <= 4.
+Proof.
+  intros;micromega Z.
+Qed.
+
+Lemma hol_light10 : forall x y,
+ x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+Lemma hol_light11 : forall x y,
+ x > 1 /\ y > 1 -> x * y > x + y - 1.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+
+Lemma hol_light12: forall x y z,
+  2 <= x /\ x <= 125841 / 50000 /\
+  2 <= y /\ y <= 125841 / 50000 /\
+  2 <= z /\ z <= 125841 / 50000
+   -> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= 0.
+Proof.
+  intros x y z ; set (e:= (125841 / 50000)).
+  compute in e.
+  unfold e ; intros ; micromega Z.
+Qed.
+
+Lemma hol_light14 : forall x y z,
+ 2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
+  -> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
+Proof.
+  intros ;micromega Z.
+Qed.
+
+(* ------------------------------------------------------------------------- *)
+(* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
+(* ------------------------------------------------------------------------- *)
+
+Lemma hol_light16 : forall x y,
+  0 <= x /\ 0 <= y /\ (x * y = 1)
+   -> x + y <= x ^ 2 + y ^ 2.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+Lemma hol_light17 : forall x y,
+  0 <= x /\ 0 <= y /\ (x * y = 1)
+   -> x * y * (x + y) <= x ^ 2 + y ^ 2.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+Lemma hol_light18 : forall x y,
+  0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
+Proof.
+  intros ; micromega Z.
+Qed.
+
+(* ------------------------------------------------------------------------- *)
+(* Some examples over integers and natural numbers.                          *)
+(* ------------------------------------------------------------------------- *)
+
+Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
+Proof.
+  intros ; zfarkas.
+Qed.
+
+Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
+Proof.
+  intros.
+  micromega Z.
+Qed.
+
+
+Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> 
+  ((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
+                -> (x1 + y1 = x2 + y2).
+Proof.
+  intros.
+  micromega Z.
+Qed.
+
+Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
+Proof.
+  intros ; sos Z.
+Qed.
+
+
+
+Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2)  >= 0.
+Proof.
+  intros.
+  generalize (motzkin' x y).
+  micromega Z.
+Qed.
diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v
new file mode 100644
index 00000000..ec88b68d
--- /dev/null
+++ b/test-suite/micromega/heap3_vcgen_25.v
@@ -0,0 +1,38 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import ZArith.
+Require Import Micromegatac.
+
+Open Scope Z_scope.
+
+Lemma vcgen_25 : forall   
+  (n : Z)
+  (m : Z)
+  (jt : Z)
+  (j : Z)
+  (it : Z)
+  (i : Z)
+  (H0 : 1 * it + -2 * i + -1 = 0)
+  (H : 1 * jt + -2 * j + -1 = 0)
+  (H1 : 1 * n + -10 = 0)
+  (H2 : 0 <= -4028 * i + 6222 * j + 705 * m + -16674)
+  (H3 : 0 <= -418 * i + 651 * j + 94 * m + -1866)
+  (H4 : 0 <= -209 * i + 302 * j + 47 * m + -839)
+  (H5 : 0 <= -1 * i + 1 * j + -1)
+  (H6 : 0 <= -1 * j + 1 * m + 0)
+  (H7 : 0 <= 1 * j + 5 * m + -27)
+  (H8 : 0 <= 2 * j + -1 * m + 2)
+  (H9 : 0 <= 7 * j + 10 * m + -74)
+  (H10 : 0 <= 18 * j + -139 * m + 1188)
+  (H11 : 0 <= 1 * i + 0)
+  (H13 : 0 <= 121 * i + 810 * j + -7465 * m + 64350),
+  (1 = -2 * i + it).
+Proof.
+  intros ; zfarkas.
+Qed.
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
new file mode 100644
index 00000000..42aff5a4
--- /dev/null
+++ b/test-suite/micromega/qexample.v
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import Micromegatac.
+Require Import QArith.
+Require Import Ring_normalize.
+
+Lemma plus_minus : forall x y, 
+  0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
+Proof.
+  intros.
+  omicron Q.
+Qed.
+
+(* Other (simple) examples *)
+Open Scope Q_scope.
+
+Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2).
+Proof.
+  intros.
+  omicron Q.
+Qed.
+
+
+Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m.
+Proof.
+  intros ; omicron Q.
+Qed.
+Open Scope Z_scope.
+Open Scope Q_scope.
+
+Lemma vcgen_25 : forall   
+  (n : Q)
+  (m : Q)
+  (jt : Q)
+  (j : Q)
+  (it : Q)
+  (i : Q)
+  (H0 : 1 * it + (-2 # 1) * i + (-1 # 1) == 0)
+  (H :  1 * jt + (-2 # 1) * j + (-1 # 1) == 0)
+  (H1 : 1 * n + (-10 # 1) = 0)
+  (H2 : 0 <= (-4028 # 1)  * i + (6222 # 1) * j + (705 # 1)  * m + (-16674 # 1))
+  (H3 : 0 <= (-418 # 1) * i + (651 # 1) * j + (94 # 1) * m + (-1866 # 1))
+  (H4 : 0 <= (-209 # 1) * i + (302 # 1) * j + (47 # 1) * m + (-839 # 1))
+  (H5 : 0 <= (-1 # 1) * i + 1 * j + (-1 # 1))
+  (H6 : 0 <= (-1 # 1) * j + 1 * m + (0 # 1))
+  (H7 : 0 <= (1 # 1) * j + (5 # 1) * m + (-27 # 1))
+  (H8 : 0 <= (2 # 1) * j + (-1 # 1) * m + (2 # 1))
+  (H9 : 0 <= (7 # 1) * j + (10 # 1) * m + (-74 # 1))
+  (H10 : 0 <= (18 # 1) * j + (-139 # 1) * m + (1188 # 1))
+  (H11 : 0 <= 1  * i + (0 # 1))
+  (H13 : 0 <= (121 # 1)  * i + (810 # 1)  * j + (-7465 # 1) * m + (64350 # 1)),
+  (( 1# 1) == (-2 # 1) * i + it).
+Proof.
+  intros.
+  omicron Q.
+Qed.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
new file mode 100644
index 00000000..5132dc4e
--- /dev/null
+++ b/test-suite/micromega/rexample.v
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import Micromegatac.
+Require Import Reals.
+Require Import Ring_normalize.
+
+Open Scope R_scope.
+
+Lemma plus_minus : forall x y, 
+  0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
+Proof.
+  intros.
+  omicron R.
+Qed.
+
+(* Other (simple) examples *)
+
+Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
+Proof.
+  intros.
+  omicron R.
+Qed.
+
+
+Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
+Proof.
+  intros ; omicron R.
+Qed.
+
+
+Lemma vcgen_25 : forall   
+  (n : R)
+  (m : R)
+  (jt : R)
+  (j : R)
+  (it : R)
+  (i : R)
+  (H0 : 1 * it + (-2%R  ) * i + (-1%R  ) = 0)
+  (H :  1 * jt + (-2  ) * j + (-1  ) = 0)
+  (H1 : 1 * n + (-10  ) = 0)
+  (H2 : 0 <= (-4028  )  * i + (6222  ) * j + (705  )  * m + (-16674  ))
+  (H3 : 0 <= (-418  ) * i + (651  ) * j + (94  ) * m + (-1866  ))
+  (H4 : 0 <= (-209  ) * i + (302  ) * j + (47  ) * m + (-839  ))
+  (H5 : 0 <= (-1  ) * i + 1 * j + (-1  ))
+  (H6 : 0 <= (-1  ) * j + 1 * m + (0  ))
+  (H7 : 0 <= (1  ) * j + (5  ) * m + (-27  ))
+  (H8 : 0 <= (2  ) * j + (-1  ) * m + (2  ))
+  (H9 : 0 <= (7  ) * j + (10  ) * m + (-74  ))
+  (H10 : 0 <= (18  ) * j + (-139  ) * m + (1188  ))
+  (H11 : 0 <= 1  * i + (0  ))
+  (H13 : 0 <= (121  )  * i + (810  )  * j + (-7465  ) * m + (64350  )),
+  (( 1 ) = (-2  ) * i + it).
+Proof.
+  intros.
+  omicron R.
+Qed.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
new file mode 100644
index 00000000..30c72e8c
--- /dev/null
+++ b/test-suite/micromega/square.v
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import ZArith Zwf Micromegatac QArith.
+Open Scope Z_scope.
+
+Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
+Proof.
+ intros ; case (Zabs_dec x) ; intros ; micromega Z.
+Qed.
+Hint Resolve Zabs_pos Zabs_square.
+
+Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
+Proof.
+intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
+assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
+         /\ Zabs p^2 = p^2) by auto.
+assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by 
+  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; micromega Z).
+generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
+intros n IHn p [Hn [Hp Heq]].
+assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; micromega Z).
+assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by micromega Z.
+apply (IHn (2*p-n) Hzwf (n-p) Hdecr).
+Qed.
+
+Open Scope Q_scope.
+
+Lemma QnumZpower : forall x : Q, Qnum (x ^ 2)%Q = ((Qnum x) ^ 2) %Z.
+Proof.
+  intros.
+  destruct x.
+  cbv beta  iota zeta delta - [Zmult].
+  ring.
+Qed.
+
+
+Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z.
+Proof.
+  intros.
+  destruct x.
+  cbv beta  iota zeta delta - [Pmult].
+  rewrite Pmult_1_r.
+  reflexivity.
+Qed.
+
+Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
+Proof.
+ unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r.
+ intros HQeq.
+ assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by 
+   (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
+ assert (Hnx : (Qnum x <> 0)%Z)
+ by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
+ apply integer_statement; exists (Qnum x); exists (' Qden x); auto.
+Qed.
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
new file mode 100644
index 00000000..b13654d6
--- /dev/null
+++ b/test-suite/micromega/zomicron.v
@@ -0,0 +1,27 @@
+Require Import ZArith.
+Require Import Micromegatac.
+Open Scope Z_scope.
+
+Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
+Proof.
+  intros.
+  omicron Z.
+Qed.
+
+Lemma two_x_y_eq_1 : forall x y, 2 * x + 2 * y = 1 -> False.
+Proof.
+  intros.
+  omicron Z.
+Qed.
+
+Lemma two_x_y_z_eq_1 : forall x y z, 2 * x + 2 * y + 2 * z= 1 -> False.
+Proof.
+  intros.
+  omicron Z.
+Qed.
+
+Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> 7 * x - 9 * y = 4 -> -10 <= 7 * x - 9 * y <= 4 -> False.
+Proof.
+  intros ; intuition auto.
+  omicron Z.
+Qed.