def small_base

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/proof.bend:151

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend as LG

151def small_base(+n: Nat, +b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> S.Ilog.small_base(n, b, hb):
152  LG.ilog_small_base(n, b, hb)