law lt_of_add_lt_add_right

bend-mathlib@0.8.1.0 · nat.bend:2788

import Base

2788# A common right summand cancels in a strict inequality: a + k < b + k implies a < b.
2789law lt_of_add_lt_add_right:
2790  for a: Nat
2791  for b: Nat
2792  for k: Nat
2793  for h: lt(Nat.add(a, k), Nat.add(b, k))
2794  lt(a, b)