Proof step 17 from proof fac-le (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  (i1 + 1) * fac(i1) ≤ (i2 + 1) * fac(i2), fac(i1) ≤ fac(i2) ↔ i1 ≤ i2, 0 ≤ i1, 0 ≤ i2, ∀ i0, j. i→n(i0) < i→n(i1 + 1) → 0 < i0 ∧ 0 < j → (fac(i0) ≤ fac(j) ↔ i0 ≤ j) ⊦ i1 ≤ i2

• Proof step 21:

  i1 ≤ i2, fac(i1) ≤ fac(i2) ↔ i1 ≤ i2, 0 ≤ i1, 0 ≤ i2, ∀ i0, j. i→n(i0) < i→n(i1 + 1) → 0 < i0 ∧ 0 < j → (fac(i0) ≤ fac(j) ↔ i0 ≤ j) ⊦ (i1 + 1) * fac(i1) ≤ (i2 + 1) * fac(i2)

Rule argument

Additional information