Proof step 12 from proof mod-div-ls (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  0 < i1, 0 ≤ i0, i1 ≤ (i0 + i1 * j0) / (j0 + 1), i0 < i1, 0 ≤ j0, 0 ≤ i2, i1 * (j0 + 1) ≤ i0 + i1 * j0, i0 < (i0 + i1 * j0) / (j0 + 1), 0 < (i0 + i1 * j0) / (j0 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: div-mult-03: j ≠ 0 ⊦ (i * j) / j = i;%mod-mult-04: j ≠ 0 ⊦ (i * j) % j = 0;%forward-lsle: ⊦ 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%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%zero-ge-add: ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); from specification int-mult%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%zero-left: ⊦ 0 * i = 0; from specification int-mult%neg-15: ⊦ i + ~ j = i - j; from specification int-abs%minus-one-02: ⊦ ~1 * i = ~ i; from specification int-mult%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%mone-06: ⊦ ~1 < i ↔ 0 ≤ i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs%succ-02: ⊦ i < j + 1 ↔ i ≤ j; from specification int-abs%ler: ⊦ i ≤ i; from specification int-abs%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%numadd-01: ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; from specification int-abs