| ⊦ 0 < i → (i ^ j ≤ 0 ↔ i ^ j = 0) |
Used simplifier rules: notneg-02: ⊦ 0 < i → ¬ i ^ j < 0;%pot-zero-01: ⊦ 0 < i → (i ^ j = 0 ↔ j < 0 ∧ 1 < i);%Pot-neg: ⊦ i < 0 → j ^ i = 1 / j ^ abs(i);%zero-02: ⊦ j < 0 → (i ^ ~ j = 0 ↔ i = 0);%eqone-02: ⊦ i ^ ~ j = 1 ∧ j < 0 → abs(i) = 1;%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%abs-16: ⊦ 0 < j → abs(j) = j; from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%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%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%one-pos: j ≠ 0 ⊦ 0 < 1 / j ↔ j = 1; from specification int-div%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs