| j < 0, i / (0 - j) * (0 - j) < 0, i < 0, i / (0 - j) * (0 - j) < i, i / (0 - j) * (0 - j) < ~1 ⊦ j = 0 |
j + 1 < i / j, 0 < i / j, i < i / j, i + 1 < i / j, i < 0, j * i / j < i, j * i / j < ~1, j < 0, j < i / j ⊦ j = 0
Used simplifier rules: Div-right: ⊦ j ≠ 0 → i / ~ j = ~(i / j);%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%lsone: ⊦ i < 1 ↔ i ≤ 0; from specification int-abs%ls-same: ⊦ 0 < i → (i * j < i ↔ j < 1); from specification int-mult%lst-04: ⊦ i + j < i0 ∧ j0 < j → i + j0 < i0; 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%numlelsdel: j0 ≠ 0, j ≤ j0 ⊦ i < (* j) → i < (* j0); from specification int-abs%numls-03: ⊦ i + (* j) < (* j0) ↔ i < j0 - j; from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); from specification int-mult%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%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%numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1%zero-ls-01: ⊦ i < 0 → (i * j < 0 ↔ 0 < j); from specification int-mult%neg-02: ⊦ ~ ~ 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%minus-left: ⊦ ~ i * j = ~(i * j); from specification int-mult%neg-06: ⊦ 0 - i = ~ i; from specification int-abs