DEFINITION minus_n_n()
TYPE =
       ∀n:nat.(eq nat O (minus n n))
BODY =
Show proof