(* Title: HOL/IOA/NTP/Lemmas.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind License: GPL (GNU GENERAL PUBLIC LICENSE) Arithmetic lemmas. *) Lemmas = NatArith