law add_lt_add_right

bend-mathlib@0.8.1.0 · nat.bend:2728

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

2728# Adding on the right preserves the strict order: a < b implies a + k < b + k.
2729law add_lt_add_right:
2730  for a: Nat
2731  for b: Nat
2732  for k: Nat
2733  for h: lt(a, b)
2734  lt(Nat.add(a, k), Nat.add(b, k))

Uses (5)

Used by (2)