for b1, b2, c being Nat st b2 <= c holds
b2 - b1 <= c