def e_lt64

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:575

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/math/natural/arith.bend as NR

575# bl <= 64 gives 1 + bl / (2 + kp) < 64
576def e_lt64(+kp: Nat, +bl: Nat, +hbl: {Nat.is_le(bl, 64n) == True{} : Bool}) -> {Nat.is_lt(1n+Nat.div(bl, 2n+kp), 64n) == True{} : Bool}:
577  +x = Nat.div(bl, 2n+kp)
578  +hx = Equal.trans(Bool, Nat.is_le(Nat.mul(x, 2n+kp), bl), Nat.is_le(x, x), True{}, Equal.sym(Bool, Nat.is_le(x, x), Nat.is_le(Nat.mul(x, 2n+kp), bl), NR.le_div(1n+kp, x, bl)), N.le_refl(x))
579  +d = N.le_trans(Nat.double(x), bl, 64n, N.le_trans(Nat.double(x), Nat.mul(x, 2n+kp), bl, dbl_le_mul(x, kp), hx), hbl)
580  N.le_lt_trans(1n+x, 33n, 64n, dle(x, 32n, d), {==})