def sc_mono

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

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

93# 2^a <= 2^b for a <= b, with b = d + a
94def sc_mono(+d: Nat, +a: Nat, +x: Nat) -> {Nat.is_le(WD.sc(a, x), WD.sc(Nat.add(d, a), x)) == True{} : Bool}:
95  %sc_sc(d, a, x) : {Nat.is_le(WD.sc(a, x), _) == True{} : Bool}
96  AR.le_sc(d, WD.sc(a, x))