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.
