Proof step 16 from proof auxexdivmod (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  i < (i0 + i2 - 1) * j, i0 * j ≤ i, 0 ≤ i, 0 < j, 0 ≤ i0, i0 * j + i2 * j ≤ i, 0 < i0 + i2, 1 < i0 + i2, 1 < i2, 0 < i2, 0 ≤ i2, i0 * j + i2 * j < (i0 + i2 - 1) * j, ∀ i1, j0, i3. i1 * j0 ≤ i3 ∧ i3 < i1 * j0 + i2 * j0 ∧ 0 ≤ i1 ∧ 0 < j0 ∧ 0 ≤ i3 → (∃ i4. i4 * j0 ≤ i3 ∧ i3 < i4 * j0 + j0 ∧ 0 ≤ i4) ⊦ ∃ i1. i1 * j ≤ i ∧ i < i1 * j + j ∧ 0 ≤ i1

Rule argument

Additional information

Used simplifier rules: dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j;%associativity: ⊦ i * j * j0 = (i * j) * j0;%commutativity: ⊦ i * j = j * i;%one: ⊦ 1 * i = i;%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j);%ls-pos: ⊦ 0 < i → (i * j < i * j0 ↔ j < j0);%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%leone: ⊦ 1 ≤ i ↔ 0 < i; from specification int-abs%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%sub-add-01: ⊦ i + (j - i0) = i + j - i0; from specification int-abs%sub-pred: ⊦ i -1 = i - 1; from specification int-abs