Tactics and automation

Exercises

• Exercise 7.1 page 204 Some lemmas about divisibility
• Exercise 7.2 page 209 Rewriting with exceptions
• using omega Using omega
• New ! On pattern matching in Ltac

Errata

1. Page 195, section 7.3.2:
   read: "The subst tactic looks for hypotheses of the form x = exp or exp = x "
2. Page 196, end of the first paragraph: read: "It is however, a good complement to our caseEq tactic ..."
3. SEction 7.1.2.2, pargraph 2, page 189:
   read "Moreover, the argument delta" instead of "Moreover, the argument Delta"