DEFINITION arith0()
TYPE =
       ∀h2:nat
         .∀d2:nat
           .∀n:nat.(le (plus d2 h2) n)→∀h1:nat.(le (plus d2 h1) (minus (plus n h1) h2))
BODY =
Show proof