def fits_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:30

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

30# fits(k, n) is n < 2^k
31def fits_lt(+k: Nat, +n: Nat) -> {C.fits(k, n) == Nat.is_lt(n, C.pow2(k)) : Bool}:
32  match k:
33    case 0n:
34      match n:
35        case 0n:
36          {==}
37        case 1n+ +np:
38          Equal.sym(Bool, Nat.is_lt(np, 0n), False{}, N.not_lt_zero(np))
39    case 1n+ +p:
40      %Equal.sym(Bool, C.fits(p, C.half(n)), Nat.is_lt(C.half(n), C.pow2(p)), fits_lt(p, C.half(n))) : {_ == Nat.is_lt(n, Nat.double(C.pow2(p))) : Bool}
41      lt_half(n, C.pow2(p))