| ⊦ i→n(i) < i→n(i + 1) ↔ 0 ≤ i |
Used simplifier rules: rax-04: ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1;%abs-zero: ⊦ i→n(i) = 0 ↔ i = 0;%abs-pred-01: ⊦ i < 0 ∧ i ≠ ~1 → i→n(i + 1) = i→n(i) -1;%num-i2n-le-03: i < 0 ⊦ (* m) ≤ i→n(i) ↔ n→i(m) ≤ ~ i;%l-02: ⊦ ¬ m + n < m; from specification nat-basic2%ls: n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; from specification nat%neg: ⊦ 0 < ~ i ↔ i < 0; from specification int-abs%leone: ⊦ 1 ≤ i ↔ 0 < i; from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%pred-03: ⊦ n -1 = n - 1; from specification nat%numadd-01: ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; from specification int-abs%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%ref-1: ⊦ ¬ n < n; from specification nat-basic1%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2