DEFINITION plus_plus()
TYPE =
       ∀z:nat
         .∀x1:nat
           .∀x2:nat
             .∀y1:nat
               .∀y2:nat
                 .le x1 z
                   →(le x2 z
                        →(eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)
                             →eq nat (plus x1 y2) (plus x2 y1)))
BODY =
Show proof