Theory EnumTypeContext

Parents

Contents

Type operators

(none)

Constants

(none)

Definitions

(none)

Theorems

n_less_cases

Theorems

n_less_cases
⊢ ∀m n. n < m ⇔ m ≠ 0 ∧ (let x = m − 1 in n < x ∨ n = x)