~/jendhub

law lt_add_of_pos_left

bend-mathlib@0.8.1.0 · nat.bend:2702

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

2702# Adding a positive amount on the left strictly increases: n < (1 + k) + n.
2703law lt_add_of_pos_left:
2704  for n: Nat
2705  for k: Nat
2706  lt(n, Nat.add(1n+k, n))

Uses (5)

Used by (0)

No other definition uses this definition.