~/jendhub

def lt_add2

bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:280

import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as Lemire
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WI

280# a <= b and c < d give a + c < b + d
281def lt_add2(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +hcd: {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}:
282  N.le_lt_trans(Nat.add(a, c), Nat.add(b, c), Nat.add(b, d), WI.le_add_r(a, b, c, hab), N.lt_add_left(c, d, b, hcd))

Uses (8)

Used by (1)