def le_add2

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/num.bend:79

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

79def le_add2(+x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_le(x, a) == True{} : Bool}, +hy: {Nat.is_le(y, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(x, y), Nat.add(a, b)) == True{} : Bool}:
80  N.le_trans(Nat.add(x, y), Nat.add(a, y), Nat.add(a, b), le_add_r(x, a, y, hx), N.le_add_left(y, b, a, hy))