Scalarops.lt_p_half: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as Scalarops
Lines 178-183 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&start_line=178&end_line=183

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/crypto/secp256k1/ineq.bend as I

# small k < 2^32 is below p
def lt_p_half(+h: Nat, +m: Nat, +c: Nat, +e: {Nat.add(m, c) == Nat.add(h, h) : Nat}, +hc: {Nat.is_le(c, h) == True{} : Bool}) -> {Nat.is_le(h, m) == True{} : Bool}:
  +s1 = N.le_add_left(c, h, h, hc)
  +s2 = I.le_subst_r(Nat.add(h, c), Nat.add(h, h), Nat.add(m, c), Equal.sym(Nat, Nat.add(m, c), Nat.add(h, h), e), s1)
  +s3 = Equal.trans(Bool, Nat.is_le(h, m), Nat.is_le(Nat.add(h, c), Nat.add(m, c)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(h, c), Nat.add(m, c)), Nat.is_le(h, m), le_cancel_r(h, m, c)), s2)
  s3

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=le_subst_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=le_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_left