law add_le_add

bend-mathlib@0.8.1.0 · nat.bend:1528

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

import Base

1528# Adding two bounded summands stays bounded: a <= c and b <= d imply a + b <= c + d.
1529law add_le_add:
1530  for +a: Nat
1531  for +b: Nat
1532  for +c: Nat
1533  for +d: Nat
1534  for h1: le(a, c)
1535  for h2: le(b, d)
1536  le(Nat.add(a, b), Nat.add(c, d))

Uses (6)

Used by (3)