7 files changed, 122 insertions, 4 deletions
diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v
new file mode 100644
index 0000000000..e62b5b8d9e
--- /dev/null
+++ b/test-suite/micromega/bug_11089.v
@@ -0,0 +1,13 @@
+Require Import Lia.
+Unset Lia Cache.
+Definition t := nat.
+Goal forall (n : t), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
+Goal let t' := nat in forall (n : t'), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/bug_11656.v b/test-suite/micromega/bug_11656.v
new file mode 100644
index 0000000000..19846ad50a
--- /dev/null
+++ b/test-suite/micromega/bug_11656.v
@@ -0,0 +1,11 @@
+Require Import Lia.
+Require Import NArith.
+Open Scope N_scope.
+
+Goal forall (a b c: N),
+    a <> 0 ->
+    c <> 0 ->
+    a * ((b + 1) * c) <> 0.
+Proof.
+  intros. nia.
+Qed.
diff --git a/test-suite/micromega/bug_12184.v b/test-suite/micromega/bug_12184.v
new file mode 100644
index 0000000000..d329a3fa7f
--- /dev/null
+++ b/test-suite/micromega/bug_12184.v
@@ -0,0 +1,8 @@
+Require Import Lia.
+Require Import ZArith.
+
+Goal forall p : positive, (0 < Z.pos (2^p)%positive)%Z.
+Proof.
+  intros p.
+  lia.
+Qed.
diff --git a/test-suite/micromega/bug_14054.v b/test-suite/micromega/bug_14054.v
new file mode 100644
index 0000000000..d97e13375f
--- /dev/null
+++ b/test-suite/micromega/bug_14054.v
@@ -0,0 +1,46 @@
+(* bug 13242 *)
+
+Require Import Lia.
+Fail Add Zify InjTyp id.
+
+(* bug 14054 *)
+
+Require Import Coq.ZArith.ZArith. Open Scope Z_scope.
+Require Coq.Init.Byte .
+Require Import Coq.micromega.ZifyClasses Coq.micromega.Lia.
+
+Notation byte := Coq.Init.Byte.byte.
+
+Module byte.
+  Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).
+End byte.
+
+Section WithA.
+  Context (A: Type).
+  Fixpoint tuple(n: nat): Type :=
+    match n with
+    | O => unit
+    | S m => A * tuple m
+    end.
+End WithA.
+
+Module LittleEndian.
+  Fixpoint combine (n : nat) : forall (bs : tuple byte n), Z :=
+    match n with
+    | O => fun _ => 0
+    | S n => fun bs => Z.lor (byte.unsigned (fst bs))
+                             (Z.shiftl (combine n (snd bs)) 8)
+    end.
+  Lemma combine_bound: forall {n: nat} (t: tuple byte n),
+      0 <= LittleEndian.combine n t < 2 ^ (8 * Z.of_nat n).
+  Admitted.
+End LittleEndian.
+
+Instance InjByteTuple{n: nat}: InjTyp (tuple byte n) Z := {|
+  inj := LittleEndian.combine n;
+  pred x := 0 <= x < 2 ^ (8 * Z.of_nat n);
+  cstr := @LittleEndian.combine_bound n;
+|}.
+Fail Add Zify InjTyp InjByteTuple.
+Fail Add Zify UnOp InjByteTuple.
+Fail Add Zify UnOp X.
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index d70bb809c6..d22e2b7c8c 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -12,6 +12,12 @@ Open Scope Z_scope.
 Require Import ZMicromega.
 Require Import VarMap.
 
+Lemma power_pos : forall x y, 0 <= x \/ False -> x^ y >= 0.
+Proof.
+  intros.
+  lia.
+Qed.
+
 Lemma not_so_easy : forall x n : Z,
   2*x + 1 <= 2 *n -> x <= n-1.
 Proof.
diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v
index 485c24f0c9..e79b76b810 100644
--- a/test-suite/micromega/example_nia.v
+++ b/test-suite/micromega/example_nia.v
@@ -7,10 +7,16 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Psatz.
 Open Scope Z_scope.
-Require Import ZMicromega.
+Require Import ZMicromega Lia.
 Require Import VarMap.
+Unset Nia Cache.
+
+Goal forall (x y: Z), 0 < (1+y^2)^(x^2).
+Proof. nia. Qed.
+
+Goal forall (x y: Z), 0 <= (y^2)^x.
+Proof. nia. Qed.
 
 (* false in Q : x=1/2 and n=1 *)
 
@@ -347,8 +353,8 @@ Lemma hol_light17 : forall x y,
    -> x * y * (x + y) <= x ^ 2 + y ^ 2.
 Proof.
   intros.
-  Fail nia.
-Abort.
+  nia.
+Qed.
 
 
 Lemma hol_light18 : forall x y,
@@ -507,3 +513,24 @@ Proof.
   intros.
   lia.
 Qed.
+
+Lemma mult : forall x x0 x1 x2 n n0 n1 n2,
+    0 <= x -> 0 <= x0 -> 0 <= x1 -> 0 <= x2 ->
+    0 <= n -> 0 <= n0 -> 0 <= n1 -> 0 <= n2 ->
+    (n1 * x <= n2 * x1) ->
+    (n * x0 <= n0 * x2) ->
+  (n1 * n * (x * x0) > n2 * n0 * (x1 * x2)) -> False.
+Proof.
+  intros.
+  nia.
+Qed.
+
+
+Lemma mult_nat : forall x x0 x1 x2 n n0 n1 n2,
+    (n1 * x <= n2 * x1)%nat ->
+    (n * x0 <= n0 * x2)%nat ->
+  (n1 * n * (x * x0) > n2 * n0 * (x1 * x2))%nat -> False.
+Proof.
+  intros.
+  nia.
+Qed.
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index a12623c3c0..2ea320047d 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -167,6 +167,12 @@ Goal  @zero znat = 0%nat.
   reflexivity.
 Qed.
 
+Require Import ZifyBool.
+Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
+  { TUOp := id; TUOpInj := fun _ => eq_refl }.
+Add Zify UnOp Op_bool_inj.
+
+
 Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y),
     (F P + 1 = 1 + F P)%positive.
 Proof.
@@ -228,6 +234,7 @@ Proof.
   intros. lia.
 Qed.
 
+
 Ltac Zify.zify_pre_hook ::= unfold is_true in *.
 
 Goal forall x y : nat, is_true (Nat.eqb x 1) ->