Proof step 4 from proof mod-nle (previous step)

User applied rule insert equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: zero-le: ⊦ 0 < i → (i * j ≤ 0 ↔ j ≤ 0);%associativity: ⊦ i * j * j0 = (i * j) * j0;%commutativity: ⊦ i * j = j * i;%one-01: ⊦ i = 1 → i * j = j;%zero-left: ⊦ 0 * i = 0;%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%lep-01: ⊦ i + j ≤ i ↔ j ≤ 0; from specification int-abs%sub-le: ⊦ i - j ≤ i0 ↔ i ≤ j + i0; from specification int-abs%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%bet: ⊦ 0 < i → (i ≤ 1 ↔ i = 1); from specification int-abs%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%sub-eq-01: ⊦ i = j → i - j = 0; from specification int-abs%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2