Re: [isabelle] reasoning with even and odd numbers




One possibility:

lemma "ev 4"
using evSS[OF evSS[OF ev0]]
by(simp add: numeral_eq_Suc)

Thank you.

Is there a difference between using a proof vs adding it to simp like this?

lemma "ev 4"
by (simp add: numeral_eq_Suc evSS[OF evSS[OF ev0]])

Amarin




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