def lt_le_add

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/ineq.bend:33

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

33# a < c, b <= d: a + b < c + d
34def lt_le_add(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +h1: {Nat.is_lt(a, c) == True{} : Bool}, +h2: {Nat.is_le(b, d) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), Nat.add(c, d)) == True{} : Bool}:
35  N.lt_le_trans(Nat.add(a, b), Nat.add(c, b), Nat.add(c, d), N.lt_add_r2(a, c, b, h1), N.le_add_left(b, d, c, h2))