def le_mul256
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:114
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as Fill
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/lemmas/proofs/nat_algebra.bend as NA
114def le_mul256(+n: Nat) -> {Nat.is_le(n, Nat.mul(n, 256n)) == True{} : Bool}:
115 %Equal.sym(Nat, Nat.mul(n, 256n), Nat.mul(256n, n), NA.mul_comm(n, 256n)) : {Nat.is_le(n, _) == True{} : Bool}
116 N.le_add_right(n, Nat.mul(255n, n))