(* Title: HOLCF/IOA/ABP/Lemmas.thy ID: $Id$ Author: Olaf Müller License: GPL (GNU GENERAL PUBLIC LICENSE) Arithmetic lemmas. *) Lemmas = NatArith