proofs/math/typed/natfuel.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as Natfuel

16 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./u32.bend as U32P
import ../../lib/arith.bend as AR2
import ../natural/bits.bend as BT
import ../natural/inverse.bend as IV
import ../../lib/u32half.bend as UH
import ../../../spec/math/natural.bend as S
import ../natural/fact.bend as FA
import ../natural/roots.bend as RT
import ../natural/modpow.bend as MP

Definitions

def true_ne_false source · line 25 · raw

@+h:{True{} == False{} : Bool} -> Empty

def ends source · line 31 · raw

@f:Nat -> @+a:Nat -> @+b:Nat -> Bool

the Nat loop reaches b == 0 within f steps

def ends_zero source · line 42 · raw

@+f:Nat -> @+a:Nat -> {ends(f, a, 0n) == True{} : Bool}

def gz source · line 50 · raw

@+f:Nat -> @+a:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_go(f, a, 0n) == a : Nat}

two fuels that both reach the end give the same gcd

def gcd_fuel source · line 57 · raw

@+f1:Nat -> @+f2:Nat -> @+a:Nat -> @+b:Nat -> @+h1:{ends(f1, a, b) == True{} : Bool} -> @+h2:{ends(f2, a, b) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_go(f1, a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_go(f2, a, b) : Nat}

def ends_self source · line 71 · raw

@+f:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(b, f) == True{} : Bool} -> {ends(f, a, b) == True{} : Bool}

b <= f is enough: b drops every step

def mod_le_sub source · line 81 · raw

@+b:Nat -> @+rp:Nat -> @+h:{Nat.is_le(1n+rp, b) == True{} : Bool} -> {Nat.is_le(Nat.add(Nat.mod(b, 1n+rp), 1n+rp), b) == True{} : Bool}

b mod r + r <= b for 0 < r <= b (the quotient is at least 1)

def halve2 source · line 93 · raw

@+b:Nat -> @+r1:Nat -> @+r2:Nat -> @+k:Nat -> @+hb:{Nat.is_lt(b, Nat.double(k)) == True{} : Bool} -> @+h21:{Nat.is_lt(r2, r1) == True{} : Bool} -> @+hs:{Nat.is_le(Nat.add(r2, r1), b) == True{} : Bool} -> {Nat.is_lt(r2, k) == True{} : Bool}

two remainders later the divisor has at least halved

def halve source · line 99 · raw

@+k:Nat -> @+f:Nat -> @+a:Nat -> @+b:Nat -> @+r:Nat -> @+hr:{Nat.mod(a, b) == r : Nat} -> @+hb:{Nat.is_lt(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hf:{Nat.is_le(1n+Nat.double(k), f) == True{} : Bool} -> {ends(f, a, b) == True{} : Bool}

Knuth: b < 2^k and 2k + 1 <= f reach the end (r is a mod b, given)

def gcd_140 source · line 124 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+hk:{Nat.is_le(1n+Nat.double(k), 140n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd_go(140n, a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.gcd(a, b) : Nat}

140 steps are enough for Euclid on values below 2^k, 2k + 1 <= 140

def bends source · line 129 · raw

@f:Nat -> @+n:Nat -> Bool

def bends_zero source · line 140 · raw

@+f:Nat -> {bends(f, 0n) == True{} : Bool}

def half_below source · line 148 · raw

@+n:Nat -> @+p:Nat -> @+h:{Nat.is_lt(n, Nat.double(p)) == True{} : Bool} -> {Nat.is_lt(Nat.div(n, 2n), p) == True{} : Bool}

div(n, 2) < p when n < 2p

def bends_bound source · line 154 · raw

@+j:Nat -> @+f:Nat -> @+n:Nat -> @+hn:{Nat.is_lt(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(j)) == True{} : Bool} -> @+hf:{Nat.is_le(j, f) == True{} : Bool} -> {bends(f, n) == True{} : Bool}

n < 2^j and j <= f: f halvings reach 0

def bends_self source · line 166 · raw

@+f:Nat -> @+n:Nat -> @+h:{Nat.is_le(n, f) == True{} : Bool} -> {bends(f, n) == True{} : Bool}

n <= f is enough (n drops every step)

def bl_zero source · line 175 · raw

@+f:Nat -> @+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length_go(f, 0n, k) == k : Nat}

def bl_fuel source · line 182 · raw

@+f1:Nat -> @+f2:Nat -> @+n:Nat -> @+k:Nat -> @+h1:{bends(f1, n) == True{} : Bool} -> @+h2:{bends(f2, n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length_go(f1, n, k) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length_go(f2, n, k) : Nat}

def bl_140 source · line 194 · raw

@+j:Nat -> @+n:Nat -> @+hj:{Nat.is_le(j, 140n) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(j)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length_go(140n, n, 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) : Nat}

140 steps suffice for bit_length below 2^j, j <= 140

def pm_zero source · line 197 · raw

@+f:Nat -> @+m:Nat -> @+base:Nat -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(f, m, 0n, base, acc) == acc : Nat}

def pm_fuel source · line 204 · raw

@+f1:Nat -> @+f2:Nat -> @+m:Nat -> @+e:Nat -> @+base:Nat -> @+acc:Nat -> @+h1:{bends(f1, e) == True{} : Bool} -> @+h2:{bends(f2, e) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(f1, m, e, base, acc) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(f2, m, e, base, acc) : Nat}

def pm_140 source · line 215 · raw

@+j:Nat -> @+m:Nat -> @+e:Nat -> @+base:Nat -> @+acc:Nat -> @+hj:{Nat.is_le(j, 140n) == True{} : Bool} -> @+he:{Nat.is_lt(e, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(j)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(140n, m, e, base, acc) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(e, m, e, base, acc) : Nat}

def iv_zero source · line 220 · raw

@+f:Nat -> @+m:Nat -> @+r0:Nat -> @+s0:Nat -> @+s1:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_go(f, m, r0, s0, 0n, s1) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.BZ{r0, s0} : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout}

def inv_fuel source · line 227 · raw

@+f1:Nat -> @+f2:Nat -> @+m:Nat -> @+r0:Nat -> @+s0:Nat -> @+r1:Nat -> @+s1:Nat -> @+h1:{ends(f1, r0, r1) == True{} : Bool} -> @+h2:{ends(f2, r0, r1) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_go(f1, m, r0, s0, r1, s1) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_go(f2, m, r0, s0, r1, s1) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout}

def inv_140 source · line 241 · raw

@+k:Nat -> @+mp:Nat -> @+a:Nat -> @+hk:{Nat.is_le(1n+Nat.double(k), 140n) == True{} : Bool} -> @+hm:{Nat.is_lt(1n+mp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_go(140n, 1n+mp, 1n+mp, 0n, Nat.mod(a, 1n+mp), 1n) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.inv_go(1n+mp, 1n+mp, 1n+mp, 0n, Nat.mod(a, 1n+mp), 1n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.Bezout}

fuel 140 against the reference fuel m, for m < 2^k, 2k+1 <= 140

def mod_small source · line 247 · raw

@+mp:Nat -> @+d:Nat -> @+h:{Nat.is_lt(d, 1n+mp) == True{} : Bool} -> {Nat.mod(d, 1n+mp) == d : Nat}

def sm_lt source · line 250 · raw

@+mm:Nat -> @+s:Nat -> @+x:Nat -> @+h:{Nat.is_lt(s, x) == True{} : Bool} -> @+hx:{Nat.is_le(x, mm) == True{} : Bool} -> {Nat.is_lt(Nat.add(s, Nat.sub(mm, x)), mm) == True{} : Bool}

def sm_ge source · line 253 · raw

@+mp:Nat -> @+s:Nat -> @+x:Nat -> @+hxs:{Nat.is_le(x, s) == True{} : Bool} -> @+hs:{Nat.is_lt(s, 1n+mp) == True{} : Bool} -> {Nat.mod(Nat.add(s, Nat.sub(1n+mp, x)), 1n+mp) == Nat.sub(s, x) : Nat}

def ilends source · line 265 · raw

@f:Nat -> @+q:Nat -> @+b:Nat -> @+p:Nat -> @+up:Bool -> Bool

def il_false source · line 276 · raw

@+f:Nat -> @+q:Nat -> @+b:Nat -> @+p:Nat -> {ilends(f, q, b, p, False{}) == True{} : Bool}

def ilz source · line 283 · raw

@+f:Nat -> @+n:Nat -> @+b:Nat -> @+k:Nat -> @+p:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_go(f, n, b, k, p, False{}) == k : Nat}

def il_fuel source · line 290 · raw

@+f1:Nat -> @+f2:Nat -> @+n:Nat -> @+b:Nat -> @+k:Nat -> @+p:Nat -> @+up:Bool -> @+h1:{ilends(f1, Nat.div(n, b), b, p, up) == True{} : Bool} -> @+h2:{ilends(f2, Nat.div(n, b), b, p, up) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_go(f1, n, b, k, p, up) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_go(f2, n, b, k, p, up) : Nat}

def pow2_pos source · line 303 · raw

@+x:Nat -> {Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(x)) == True{} : Bool}

def lt_pow2 source · line 310 · raw

@+x:Nat -> {Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(x)) == True{} : Bool}

def dbl_le_mul source · line 317 · raw

@+p:Nat -> @+bq:Nat -> {Nat.is_le(Nat.double(p), Nat.mul(p, 2n+bq)) == True{} : Bool}

def ilb source · line 325 · raw

@+t:Nat -> @+f:Nat -> @+c:Bool -> @+q:Nat -> @+bq:Nat -> @+s:Nat -> @+p:Nat -> @+K:Nat -> @+hK:{Nat.add(t, s) == K : Nat} -> @+hq:{Nat.is_lt(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K)) == True{} : Bool} -> @+hs:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(s), p) == True{} : Bool} -> @+ht:{Nat.is_le(t, f) == True{} : Bool} -> @+hc:{c == Nat.is_le(p, q) : Bool} -> {ilends(f, q, 2n+bq, p, c) == True{} : Bool}

q < 2^K, 2^s <= p, t + s == K: the loop from p stops within t rounds

def il_140 source · line 341 · raw

@+K:Nat -> @+n:Nat -> @+bq:Nat -> @+hK:{Nat.is_le(K, 140n) == True{} : Bool} -> @+hq:{Nat.is_lt(Nat.div(n, 2n+bq), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_go(140n, n, 2n+bq, 0n, 1n, Nat.is_le(1n, Nat.div(n, 2n+bq))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.ilog_go(n, n, 2n+bq, 0n, 1n, Nat.is_le(1n, Nat.div(n, 2n+bq))) : Nat}

def fstep source · line 347 · raw

@+y:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(1n+y)) == True{} : Bool}

def mul_le_r source · line 352 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(Nat.mul(a, b), Nat.mul(a, c)) == True{} : Bool}

def fmono source · line 357 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(b)) == True{} : Bool}

def pf_le source · line 368 · raw

@+k:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(1n+k)) == True{} : Bool}

def fbig source · line 378 · raw

@+k:Nat -> @+i:Nat -> @+h:{Nat.is_le(1n+k, i) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.factorial(i)) == True{} : Bool}

1 + k <= i gives 2^k <= i!

def sub_mono_l source · line 383 · raw

@+m:Nat -> @+n:Nat -> @+j:Nat -> @+h:{Nat.is_le(m, n) == True{} : Bool} -> {Nat.is_le(Nat.sub(m, j), Nat.sub(n, j)) == True{} : Bool}

def dmono1 source · line 394 · raw

@+m:Nat -> @+n:Nat -> @+j:Nat -> @+h:{Nat.is_le(m, n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(m, j), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, j)) == True{} : Bool}

def dstep source · line 401 · raw

@+n:Nat -> @+s:Nat -> @+h:{Nat.is_lt(s, n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, s), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, 1n+s)) == True{} : Bool}

def dmono source · line 405 · raw

@+n:Nat -> @+j:Nat -> @+d:Nat -> @+h:{Nat.is_le(Nat.add(j, d), n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, j), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, Nat.add(j, d))) == True{} : Bool}

def desc_zero source · line 417 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_lt(n, k) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, k) == 0n : Nat}

def dbig source · line 421 · raw

@+k:Nat -> @+n:Nat -> @+j:Nat -> @+hj:{Nat.is_le(1n+k, j) == True{} : Bool} -> @+hjn:{Nat.is_le(j, n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/natural.desc(n, j)) == True{} : Bool}

1 + k <= j <= n gives 2^k <= n.desc(j)

def msn source · line 427 · raw

@bit:Bool -> @+na:Nat -> @+nb:Nat -> Nat

def sqn source · line 434 · raw

@more:Bool -> @+nb:Nat -> Nat

def pw_bit source · line 441 · raw

@+r:Nat -> @+na:Nat -> @+nb:Nat -> @+p2:Nat -> @+hr:{Nat.is_lt(r, 2n) == True{} : Bool} -> {Nat.mul(msn(Nat.is_eq(r, 1n), na, nb), p2) == Nat.mul(na, Nat.mul(p2, Nat.pow(nb, r))) : Nat}

def powstep source · line 450 · raw

@+j:Nat -> @+na:Nat -> @+nb:Nat -> {Nat.mul(msn(Nat.is_eq(Nat.mod(1n+j, 2n), 1n), na, nb), Nat.pow(sqn(Nat.is_lt(1n, 1n+j), nb), Nat.div(1n+j, 2n))) == Nat.mul(na, Nat.pow(nb, 1n+j)) : Nat}

def half_le source · line 465 · raw

@+j:Nat -> {Nat.is_le(Nat.div(1n+j, 2n), j) == True{} : Bool}

def plus1 source · line 469 · raw

@+x:Nat -> {Nat.add(x, 1n) == 1n+x : Nat}

def pow_mono source · line 474 · raw

@+x:Nat -> @+y:Nat -> @+k:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> {Nat.is_le(Nat.pow(x, k), Nat.pow(y, k)) == True{} : Bool}

def lt_add_cancel source · line 481 · raw

@+d:Nat -> @+x:Nat -> @+y:Nat -> {Nat.is_lt(Nat.add(d, x), Nat.add(d, y)) == Nat.is_lt(x, y) : Bool}

def dle_c source · line 488 · raw

@+q:Nat -> @+p:Nat -> @+h:{Nat.is_le(Nat.double(q), Nat.double(p)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(p, q) == c : Bool} -> {Nat.is_le(q, p) == True{} : Bool}

def dle source · line 496 · raw

@+q:Nat -> @+p:Nat -> @+h:{Nat.is_le(Nat.double(q), Nat.double(p)) == True{} : Bool} -> {Nat.is_le(q, p) == True{} : Bool}

2 q <= 2 p gives q <= p

def w_lo source · line 500 · raw

@+w:Nat -> @+p:Nat -> @+hw:{Nat.is_le(w, Nat.double(p)) == True{} : Bool} -> {Nat.is_le(Nat.div(w, 2n), p) == True{} : Bool}

w <= 2 p gives w / 2 <= p

def w_r source · line 506 · raw

@+q:Nat -> @+r:Nat -> @+p:Nat -> @+hr:{Nat.is_lt(r, 2n) == True{} : Bool} -> @+hw:{Nat.is_le(Nat.add(Nat.double(q), r), Nat.double(p)) == True{} : Bool} -> {Nat.is_le(Nat.add(q, r), p) == True{} : Bool}

def w_hi source · line 519 · raw

@+w:Nat -> @+p:Nat -> @+hw:{Nat.is_le(w, Nat.double(p)) == True{} : Bool} -> {Nat.is_le(Nat.sub(w, Nat.div(w, 2n)), p) == True{} : Bool}

w <= 2 p gives w - w / 2 <= p

def root_below_c source · line 529 · raw

@+r:Nat -> @+x:Nat -> @+k:Nat -> @+n:Nat -> @+hx:{Nat.is_le(Nat.pow(x, k), n) == True{} : Bool} -> @+hr:{Nat.is_lt(n, Nat.pow(1n+r, k)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(r, x) == c : Bool} -> {Nat.is_le(x, r) == True{} : Bool}

x^k <= n < (1 + r)^k gives x <= r

def root_below source · line 537 · raw

@+r:Nat -> @+x:Nat -> @+k:Nat -> @+n:Nat -> @+hx:{Nat.is_le(Nat.pow(x, k), n) == True{} : Bool} -> @+hr:{Nat.is_lt(n, Nat.pow(1n+r, k)) == True{} : Bool} -> {Nat.is_le(x, r) == True{} : Bool}

def root_above_c source · line 541 · raw

@+r:Nat -> @+x:Nat -> @+k:Nat -> @+n:Nat -> @+hx:{Nat.is_le(Nat.pow(x, k), n) == False{} : Bool} -> @+hr:{Nat.is_le(Nat.pow(r, k), n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(x, r) == c : Bool} -> {Nat.is_lt(r, x) == True{} : Bool}

x^k > n >= r^k gives r < x

def root_above source · line 548 · raw

@+r:Nat -> @+x:Nat -> @+k:Nat -> @+n:Nat -> @+hx:{Nat.is_le(Nat.pow(x, k), n) == False{} : Bool} -> @+hr:{Nat.is_le(Nat.pow(r, k), n) == True{} : Bool} -> {Nat.is_lt(r, x) == True{} : Bool}

def bl_le_c source · line 552 · raw

@+K:Nat -> @+bl:Nat -> @+h:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(bl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(1n+K)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(1n+K, bl) == c : Bool} -> {Nat.is_le(bl, K) == True{} : Bool}

n < 2^K gives bit_length(n) <= K

def bl_le_n source · line 559 · raw

@+K:Nat -> @+n:Nat -> @+hn:{Nat.is_lt(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K)) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), K) == True{} : Bool}

def e_lt source · line 569 · raw

@+kp:Nat -> @+bl:Nat -> @+hbl:{Nat.is_le(bl, 32n) == True{} : Bool} -> {Nat.is_lt(1n+Nat.div(bl, 2n+kp), 32n) == True{} : Bool}

bl <= 32 gives 1 + bl / (2 + kp) < 32

def e_lt64 source · line 576 · raw

@+kp:Nat -> @+bl:Nat -> @+hbl:{Nat.is_le(bl, 64n) == True{} : Bool} -> {Nat.is_lt(1n+Nat.div(bl, 2n+kp), 64n) == True{} : Bool}

bl <= 64 gives 1 + bl / (2 + kp) < 64