def sum_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldops.bend:39

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

39def sum_lt(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_lt(b, C.shift(256n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
40  +t = C.shift(256n, one)
41  lt3(one, h1, Nat.add(a, b), I.lt_le_add(a, b, t, Nat.add(t, t), ha, N.le_trans(b, t, Nat.add(t, t), N.lt_le(b, t, hb), N.le_add_right(t, t))))