def bound_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64div.bend:183

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

183# Q <= Y < B with B == n * S gives Q < S * n2 for n == n2. The bound stays
184# 2^32 * v(d) with v(d) opaque: 2^32 * (1 + dp) would unfold into 2^32
185# successors.
186def bound_lt(+q: Nat, +y: Nat, +b: Nat, +s: Nat, +n: Nat, +n2: Nat, +hn: {n == n2 : Nat}, +hb: {Nat.mul(n, s) == b : Nat}, +hqy: {Nat.is_le(q, y) == True{} : Bool}, +hyb: {Nat.is_lt(y, b) == True{} : Bool}) -> {Nat.is_lt(q, Nat.mul(s, n2)) == True{} : Bool}:
187  +e = Equal.trans(Nat, b, Nat.mul(n, s), Nat.mul(s, n), Equal.sym(Nat, Nat.mul(n, s), b, hb), NA.mul_comm(n, s))
188  +lt = L.subst(Nat, z => {Nat.is_lt(q, z) == True{} : Bool}, b, Nat.mul(s, n), e, N.le_lt_trans(q, y, b, hqy, hyb))
189  L.subst(Nat, z => {Nat.is_lt(q, Nat.mul(s, z)) == True{} : Bool}, n, n2, hn, lt)