DEFINITION le_plus_minus_r()
TYPE =
∀n:nat.∀m:nat.(le n m)→(eq nat (plus n (minus m n)) m)
BODY =
assume n: nat
assume m: nat
suppose H: le n m
by (le_plus_minus . . H)
we proved eq nat m (plus n (minus m n))
by (sym_eq . . . previous)
we proved eq nat (plus n (minus m n)) m
we proved ∀n:nat.∀m:nat.(le n m)→(eq nat (plus n (minus m n)) m)