3 files changed, 26 insertions, 7 deletions
diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v
new file mode 100644
index 0000000000..fc6ccbb233
--- /dev/null
+++ b/test-suite/micromega/bug_11436.v
@@ -0,0 +1,19 @@
+Require Import ZArith Lia.
+Local Open Scope Z_scope.
+
+Unset Lia Cache.
+
+Goal forall a q q0 q1 r r0 r1: Z,
+    0 <= a < 2 ^ 64 ->
+    r1 = 4 * q + r ->
+    0 <= r < 4 ->
+    a = 4 * q0 + r0 ->
+    0 <= r0 < 4 ->
+    a + 4 = 2 ^ 64 * q1 + r1 ->
+    0 <= r1 < 2 ^ 64 ->
+    r = r0.
+Proof.
+  intros.
+  (* subst. *)
+  Time lia.
+Qed.
diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v
new file mode 100644
index 0000000000..a53c160e45
--- /dev/null
+++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v
@@ -0,0 +1,4 @@
+Require Import Lia.
+Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3,
+  (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)).
+Proof. eexists _, _, _. Fail lia. Abort.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 9efb81a901..36b4243ef8 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,15 +11,14 @@ Open Scope Z_scope.
 
 Lemma Zabs_square : forall x,  (Z.abs  x)^2 = x^2.
 Proof.
- intros ; case (Zabs_dec x) ; intros ; nia.
+ intros ; nia.
 Qed.
-Hint Resolve Z.abs_nonneg Zabs_square.
 
 Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
 Proof.
   intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
 assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
-         /\ Z.abs p^2 = p^2) by auto.
+         /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
   (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
@@ -45,10 +44,7 @@ Proof.
   intros.
   destruct x.
   simpl.
-  unfold Z.pow_pos.
-  simpl.
-  rewrite Pos.mul_1_r.
-  reflexivity.
+  lia.
 Qed.
 
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.