| i * i0 ≤ 0, j * i1 < 0, i1 < 0, gcd(i, j) = 1, i * i0 = j * i1 + 1, 0 < j, 1 < j, 0 < i, 1 < i, 0 ≤ i0 ⊦ (i * i0) % j = 1 |
Used simplifier rules: succ-01: ⊦ i +1 = i + 1; from specification int-basic2%mod-zero-04: j ≠ 0 ⊦ 0 % j = 0; from specification int-div%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%negeq: ⊦ ~ i = j ↔ i + j = 0; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%abs-neg: ⊦ abs(~ i) = abs(i); from specification int-abs%eq-one-neg: ⊦ i * j = ~1 ↔ abs(i) = 1 ∧ i = ~ j; from specification int-mult%numadd-01: ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; from specification int-abs%zero-left: ⊦ 0 * i = 0; from specification int-mult%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%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%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%zero-le: ⊦ 0 < i → (i * j ≤ 0 ↔ j ≤ 0); from specification int-mult