~/jendhub

def le_sc

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

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as Num
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR

90def le_sc(+k: Nat, +x: Nat, +a: Nat, +h: {Nat.is_le(x, a) == True{} : Bool}) -> {Nat.is_le(WD.sc(k, x), WD.sc(k, a)) == True{} : Bool}:
91  AR.sc_le(k, x, a, h)

Uses (5)

Used by (1)