Re: [isabelle] need help with quantified ints

lemma n_less_val_disj:
  "m ~= (0 :: nat) ==>
   (n < m) = (n = m - 1 | n < m - 1)"
  apply (case_tac n, simp_all)
   apply fastsimp
  apply (case_tac m, simp_all)
  apply fastsimp

As this goal only involves linear arithmetic, it can be solved automatically:
by arith


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.