DEFINITION le_minus() TYPE = ∀x:nat.∀z:nat.∀y:nat.(le (plus x y) z)→(le x (minus z y)) BODY =Show proof