def half_fuel

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/bits.bend:59

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

59# the halved argument stays within the fuel
60def half_fuel(+np: Nat, +f: Nat, +hf: {Nat.is_le(np, f) == True{} : Bool}) -> {Nat.is_le(Nat.div(1n+np, 2n), f) == True{} : Bool}:
61  N.le_trans(Nat.div(1n+np, 2n), np, f, N.lt_succ_le(Nat.div(1n+np, 2n), np, half_lt(np)), hf)