theory Theory
  imports Main
begin

lemma add_zero: "(n :: nat) + 0 = n"
  by simp

end