~/jendhub

law add_lt_add

bend-mathlib@0.8.1.0 · nat.bend:2799

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

2799# Adding two strict bounds keeps a strict bound: a < c and b < d imply a + b < c + d.
2800law add_lt_add:
2801  for a: Nat
2802  for b: Nat
2803  for c: Nat
2804  for d: Nat
2805  for h1: lt(a, c)
2806  for h2: lt(b, d)
2807  lt(Nat.add(a, b), Nat.add(c, d))

Uses (6)

Used by (1)