def step_bound

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32half.bend:137

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

137# The size after one step is at most s/2, so it stays below the halved bound.
138def step_bound(+s2: Nat, +s: Nat, +m: Nat, +hle: {Nat.is_le(s2, hlf(s)) == True{} : Bool}, +h: {Nat.is_lt(s, Nat.double(m)) == True{} : Bool}) -> {Nat.is_lt(s2, m) == True{} : Bool}:
139  N.le_lt_trans(s2, hlf(s), m, hle, hlf_lt(s, m, h))