Fix slowdown in bv_saturate from https://github.com/coq/coq/pull/17984

https://github.com/coq/coq/pull/17984 causes a significant slowdown in Islaris since the changed Z.euclidean_division_equations_cleanup function can be become very slow if there are many hypothesis of the form 0 <= ... < ... in the context. This MR works around this by changing bv_saturate to generate hypothesis of the form -1 < ... < ... instead of 0 <= ... < .... This change speeds up some case studies in Islaris by up to 30%, see here.

Since Michael is maintaining these files, I'll just merge.

Have you filed a Coq issue for this? It seems very silly that 0 <= ... vs .1 < ... would make such a big difference.

Thanks! I opened https://github.com/coq/coq/issues/18770 to hopefully fix this on the Coq side.

mentioned in commit a8c0c0f8

merged