| i0 < j, i0 ≤ 0, 0 < j, ∀ i1, j, i. i→n(i1) < i→n(i0) → 0 < j ∧ i1 ≤ 0 ∧ i1 < j → (i + i1 * j) |%| j = i |%| j ⊦ (i + i0 * j) |%| j = i |%| j, i0 < 0 ∧ i0 + 1 < j |
Used simplifier rules: lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%les: ⊦ i < j → (j ≤ i + 1 ↔ j = i + 1); 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%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%succ-02: ⊦ i < j + 1 ↔ i ≤ j; from specification int-abs%ler: ⊦ i ≤ i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs%mone-06: ⊦ ~1 < i ↔ 0 ≤ i; from specification int-abs%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%Mult-zero: ⊦ i * 0 = 0; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%ax-04: ⊦ i + 0 = i; from specification int-basic2 Used formulas: i0 = 0