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,17 @@
+- in `ENsatzTactic`
+
+  + Add new tactic `ensatz` for proving polynomial equalities
+    with existential quantifier
+    (`#160 <https://github.com/coq/stdlib/pull/160>`_,
+    by Lionel Blatter).
+
+- Add documentation for new tactic `ensatz`
+  (`#20762 <https://github.com/rocq-prover/rocq/pull/20762>`_,
+  by Lionel Blatter).
+
+- in `ENsatz`
+
+  + Add tests for 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