From ac64cad9e6c0496afc600380d5c21fd1129db400 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Tue, 5 Jan 2021 10:05:47 +0100
Subject: [micromega] Add missing support for `implb`

---
 test-suite/micromega/reify_bool.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/micromega/reify_bool.v

(limited to 'test-suite')

diff --git a/test-suite/micromega/reify_bool.v b/test-suite/micromega/reify_bool.v
new file mode 100644
index 0000000000..501fafc0b3
--- /dev/null
+++ b/test-suite/micromega/reify_bool.v
@@ -0,0 +1,18 @@
+Require Import ZArith.
+Require Import Lia.
+Import Z.
+Unset Lia Cache.
+
+Goal forall (x y : Z),
+   implb (Z.eqb x y) (Z.eqb y x) = true.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Goal forall (x y :Z), implb (Z.eqb x 0) (Z.eqb y 0) = true <->
+                      orb (negb (Z.eqb x 0))(Z.eqb y 0) = true.
+Proof.
+  intro.
+  lia.
+Qed.
-- 
cgit v1.2.3