Proof step 9 from proof div-le-same-neg (previous step)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%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-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%ls-add-02: ⊦ i * (j + j1) + i0 < i * j + j0 ↔ i * j1 + i0 < j0; from specification int-mult%one: ⊦ 1 * i = i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%ls: ⊦ i + j < j ↔ i < 0; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%modzero-03: ⊦ i < 0 ∧ j0 < j ∧ 0 < j → ¬ 0 ≤ i * j + j0; from specification int-mult%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%ls-dist-02: ⊦ i * (j + i0) + j2 < i * (j0 + i0) + j1 ↔ i * j + j2 < i * j0 + j1; from specification int-mult%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%irref: ⊦ ¬ i < i; from specification int-basic1%zero-left: ⊦ 0 * i = 0; from specification int-mult%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%abs-zero: ⊦ abs(i) ≤ 0 ↔ i = 0; from specification int-abs Used formulas: i1 = 0