Ineq.lt_add_pos: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as Ineq
Lines 77-80 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&start_line=77&end_line=80

import Base
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/lib/lemmas/proofs/nat_algebra.bend as NA

# 0 < b: a < a + b
def lt_add_pos(+a: Nat, +b: Nat, +h: {Nat.is_lt(0n, b) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(a, b)) == True{} : Bool}:
  +s = N.lt_add_left(0n, b, a, h)
  lt_subst_l(Nat.add(a, 0n), a, Nat.add(a, b), NA.add_zero(a), s)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_left