[isabelle] nat numerical constants simplifications



I have the following two lemmas:

lemma "(2 + (Suc  n)) = (3 + n)"
  by simp

lemma "f (2 + (Suc n)) = f (3 + n)"
  by simp

The first one is proved by simp, but the proof on the 
second lemma fails. How can I simplify numerical
constants in context?

Best regards,

Viorel Preoteasa




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