def prod_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:50

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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/arith.bend as LA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

50# x < 2^64: x n < 2^64 n
51def prod_lt(+x: Nat, +n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(x, n), C.shift(64n, n)) == True{} : Bool}:
52  +W = C.shift(64n, one)
53  +hw = WI.lt_one(64n, one, h1, x, hx)
54  +hle = LA.mul_le(1n+x, W, n, N.lt_succ_le_succ(x, W, hw))
55  +hlt = N.lt_le_trans(Nat.mul(x, n), Nat.mul(1n+x, n), Nat.mul(W, n), lt_plus(Nat.mul(x, n), n, hn), hle)
56  %Equal.sym(Nat, C.shift(64n, n), Nat.mul(n, W), WI.shift_mul_one(64n, one, h1, n)) : {Nat.is_lt(Nat.mul(x, n), _) == True{} : Bool}
57  %NA.mul_comm(W, n) : {Nat.is_lt(Nat.mul(x, n), _) == True{} : Bool}
58  hlt