def k38_le_t
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/reduce.bend:62
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend as Reduce
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/logic.bend as L
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/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD
62def k38_le_t(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(WD.sc(27n, one), 38n), LM.shn(32n, one)) == True{} : Bool}:
63 +a = N.le_trans(38n, 255n, WD.sc(27n, one), {==}, FD.le255(one, h1, 19n))
64 +b = M.le_add2(WD.sc(27n, one), 38n, WD.sc(27n, one), WD.sc(27n, one), N.le_refl(WD.sc(27n, one)), a)
65 +c = L.subst(Nat, z => {Nat.is_le(Nat.add(WD.sc(27n, one), 38n), z) == True{} : Bool}, Nat.add(WD.sc(27n, one), WD.sc(27n, one)), WD.sc(28n, one), M.sc_dbl(27n, one), b)
66 N.le_trans(Nat.add(WD.sc(27n, one), 38n), WD.sc(28n, one), LM.shn(32n, one), c, M.sc_mono(228n, 28n, one))