law add_lt_add_left

bend-mathlib@0.8.1.0 · nat.bend:2713

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

import Base

2713# Adding on the left preserves the strict order: a < b implies k + a < k + b.
2714law add_lt_add_left:
2715  for -a: Nat
2716  for -b: Nat
2717  for k: Nat
2718  for h: lt(a, b)
2719  lt(Nat.add(k, a), Nat.add(k, b))

Uses (3)

Used by (3)