Andres Erbsen

Given current implementation quirks this actually makes zify weaker in some cases, because saturation does not run on divisions that are converted to euclidean equations. Example from Rupicola: ```coq Lemma...

@coqbot run full ci

The test-suite failure seems to be due to saturate adding many implications to the context, causing the naive SMT solver in nia to go haywire: ```coq Require Import ZArith Lia....

Looks like we'll need a knob to be able to turn off the saturation for the test suite. My current plan is to add a post hook that clears implication...

Saturation with known premises would be sufficient to maintain completeness while zifying N. It is also necessary: goals that are true for an uninterpreted function returning N are not necessarily...

I think a global Vernac flag probably wouldn't do the job for use of lia from tactics. Ltac2 and division handling now use flag packages like [here](https://github.com/coq/coq/pull/17934/commits/1024d79ab34cb487eb456f2dcc796e34c6e49d6d), for which I...

The added change in stdlib is only needed until https://github.com/coq/coq/pull/18730 is merged, to retain zify's ability to see that Nat.div2 returns non-negative values.

@coqbot run full ci

@silene would you be willing to port Flocq over this change? Below is a draft patch that gets Flocq to build with this PR, but it probably isn't backwards compatible...

@coqbot run full ci