Proof step 3 from proof div-zero-02 (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  i + j < 0, j < 0, 0 ≤ i ⊦ i / j = 0

Rule argument

Additional information

Used simplifier rules: div-eq-zero-01: ⊦ 0 ≠ j → (i / j = 0 ↔ abs(i) < abs(j));%div-zero-05: ⊦ i < j ∧ 0 < j ∧ 0 ≤ i → i / j = 0;%ls: ⊦ i + j < j ↔ i < 0; from specification int-basic2%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%neg-07: ⊦ i < ~ j ↔ i + j < 0; from specification int-abs%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%neg: ⊦ 0 < ~ i ↔ i < 0; from specification int-abs%absls-06: ⊦ i < abs(i) ↔ i < 0; 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%absle: ⊦ 0 ≤ i → abs(i) = i; from specification int-abs%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%abs-06: ⊦ 0 < abs(i) ↔ i ≠ 0; from specification int-abs%ls-02: ⊦ i < i + j ↔ 0 < j; 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%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (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%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs