| ⊦ j0 + j < 0 ∧ j < 0 ∧ 0 < i → ¬ 0 ≤ i * j + j0 |
Used simplifier rules: ls-same-03: ⊦ i < 0 → (i < i * j ↔ j < 1);%associativity: ⊦ i * j * j0 = (i * j) * j0;%commutativity: ⊦ i * j = j * i;%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%lsone: ⊦ i < 1 ↔ i ≤ 0; from specification int-abs%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%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-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%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%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-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs