def m38_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fold.bend:88
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as Fold
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/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
88def m38_v(+one: Nat, +h1: {one == 1n : Nat}, +c: U32, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {v(U32.mul(38, c)) == Nat.mul(38n, v(c)) : Nat}:
89 +b = N.le_trans(Nat.mul(38n, v(c)), Nat.mul(38n, WD.sc(21n, one)), WD.sc(6n, WD.sc(21n, one)), M.le_mul2(38n, v(c), 38n, WD.sc(21n, one), N.le_refl(38n), hc), m38(WD.sc(21n, one)))
90 LM.mul_v(one, h1, 38, c, N.le_lt_trans(Nat.mul(38n, v(c)), WD.sc(27n, one), WD.sc(32n, one), b, LM.sc_lt(4n, 27n, one, h1)))