Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer

Reviewed-by: mattam82
Ack-by: Zimmi48

Reviewed-by: Zimmi48
Reviewed-by: vbgl

- to zify the conclusion, we are using Tactics.apply (not rewrite)

Closes #11089

- constrain the arguments of Add Zify X to be GlobRef.t
Unset Primitive Projections so that projections are GlobRef.t.

Closes #14043

Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>

The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints.  The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.

Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once

Co-authored-by:  Andrej Dudenhefner  <mrhaandi>

Closes #12184, #11656

Reviewed-by: vbgl

The vernacular command takes a reference instead of a constr.
Moreover, the head symbol is checked i.e
Add Zify InjTyp ref checks that the referenced term has type
Intyp X1 ... Xn

Closes #14054, #13242

Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>

Reviewed-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: silene

Reviewed-by: olaure01
Ack-by: jfehrle