def m38

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fold.bend:51

import Base
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/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

51# 38 x <= 2^6 x
52def m38(+x: Nat) -> {Nat.is_le(Nat.mul(38n, x), WD.sc(6n, x)) == True{} : Bool}:
53  +a = AR.mul_le(38n, 64n, x, {==})
54  +b = Equal.trans(Nat, Nat.mul(64n, x), Nat.mul(x, 64n), WD.sc(6n, x), NA.mul_comm(64n, x), AR.mul_sc(6n, x))
55  L.subst(Nat, z => {Nat.is_le(Nat.mul(38n, x), z) == True{} : Bool}, Nat.mul(64n, x), WD.sc(6n, x), b, a)