| ⊦ i % j = 0 ∧ i + i0 < 0 ∧ i0 % j ≠ 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j + 1 |
i % j = 0, j + i ≤ 0, (i + i0) + 1 < j, i < 0, i < j, i + 1 < j, 0 ≤ i0, 0 < j, i + i0 < 0, i + i0 < j ⊦ j = 1, (i + i0) / j = i / j + i0 / j + 1, i0 % j = 0
Used simplifier rules: mod-ls-same-02: j ≠ 0 ⊦ i < i % j ↔ i < 0 ∧ (abs(j) = 1 ∨ abs(j) ≤ abs(i));%mod-one: ⊦ i % 1 = 0;%one: ⊦ i / 1 = i;%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%eq: ⊦ i = i + j ↔ j = 0; from specification int-basic2%add-in: ⊦ i + j = i + i0 ↔ j = i0; from specification int-basic2%negle-07: ⊦ i ≤ ~ j ↔ i + j ≤ 0; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%abs-16: ⊦ 0 < j → abs(j) = j; from specification int-abs%ls: ⊦ i + j < j ↔ i < 0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%numls-03: ⊦ i + (* j) < (* j0) ↔ i < j0 - j; from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs