Add new tactic "ensatz" for proving polynomial equalities with existential quantifier

Co-authored-by: Laurent Thery <[email protected]>

Author: lyonel2017

doc/changelog/02-added/160-feature-ensatz.rst

@@ -0,0 +1,13 @@
+- in `ENsatzTactic`
+
+  + Add new tactic ensatz for proving polynomial equalities
+    with existential quantifier
+    (`#160 <https://github.com/coq/stdlib/pull/160>`_,
+    by Lionel Blatter).
+
+- in `ENsatz`
+
+  + Add test for the tactic ensatz
+    (`#160 <https://github.com/coq/stdlib/pull/160>`_,
+    by Lionel Blatter).
+

doc/stdlib/hidden-files

@@ -57,6 +57,7 @@ theories/micromega/ZifyComparison.v
 theories/micromega/ZifyClasses.v
 theories/micromega/ZifyPow.v
 theories/micromega/Zify.v
+theories/nsatz/ENsatzTactic.v
 theories/nsatz/NsatzTactic.v
 theories/omega/OmegaLemmas.v
 theories/omega/PreOmega.v

doc/stdlib/index-list.html.template

@@ -297,6 +297,7 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/ZArith/Zbitwise.v
     theories/ZArith/ZModOffset.v
     theories/ZArith/ZNsatz.v
+    theories/ZArith/ZENsatz.v
     theories/Numbers/DecimalFacts.v
     theories/Numbers/DecimalNat.v
     theories/Numbers/DecimalPos.v