def shn_lt_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/reduce.bend:54

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

54# 2^256 c < 2^256 2 -> c < 2
55def shn_lt_cancel(+c: Nat, +d: Nat, +h: {Nat.is_lt(LM.shn(32n, c), LM.shn(32n, d)) == True{} : Bool}) -> {Nat.is_lt(c, d) == True{} : Bool}:
56  AR.sc_lt_cancel(256n, c, d, h)