def e_lt

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

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

568# bl <= 32 gives 1 + bl / (2 + kp) < 32
569def e_lt(+kp: Nat, +bl: Nat, +hbl: {Nat.is_le(bl, 32n) == True{} : Bool}) -> {Nat.is_lt(1n+Nat.div(bl, 2n+kp), 32n) == True{} : Bool}:
570  +x = Nat.div(bl, 2n+kp)
571  +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))
572  +d = N.le_trans(Nat.double(x), bl, 32n, N.le_trans(Nat.double(x), Nat.mul(x, 2n+kp), bl, dbl_le_mul(x, kp), hx), hbl)
573  N.le_lt_trans(1n+x, 17n, 32n, dle(x, 16n, d), {==})