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

Co-authored-by: Laurent Thery <Laurent.Thery@inria.fr>

Author: lyonel2017

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

@@ -0,0 +1,7 @@
+- `ENsatzTactic.v` and `ENsatz.v`
+
+  + Add new tactic ensatz fo proving polynimial equalities
+    with existential quantifier
+    (`#160 <https://github.com/coq/stdlib/pull/160>`_,
+    by Lionel Blatter).
+

doc/stdlib/hidden-files

@@ -59,6 +59,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