Proof step 8 from proof orderedle-all (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  ¬ a0 < a ∧ ordered≤(a0 ' + y), ordered≤(a0 ' + y) ↔ (∀ m, n. m ≤ n ∧ n < 1 + # y → ¬ (a0 ' + y)[n] < (a0 ' + y)[m]) ⊦ ∀ m, n. m ≤ n ∧ ¬ 1 + # y < n → ¬ (a ' + a0 ' + y)[n] < (a ' + a0 ' + y)[m]

• Proof step 29:

  ∀ m, n. m ≤ n ∧ ¬ 1 + # y < n → ¬ (a ' + a0 ' + y)[n] < (a ' + a0 ' + y)[m], ordered≤(a0 ' + y) ↔ (∀ m, n. m ≤ n ∧ n < 1 + # y → ¬ (a0 ' + y)[n] < (a0 ' + y)[m]) ⊦ ¬ a0 < a ∧ ordered≤(a0 ' + y)

Rule argument

Additional information