1Theory EnumTypeContext[bare] 2Ancestors 3 arithmetic 4Libs 5 HolKernel Parse boolLib numLib 6 7Theorem n_less_cases: 8 !m n. n < m <=> m <> 0 /\ (let x = m - 1 in n < x \/ (n = x)) 9Proof 10 REWRITE_TAC [LET_THM] THEN BETA_TAC THEN CONV_TAC numLib.ARITH_CONV 11QED