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