~/jendhub

def no_fuel

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/roots.bend:140

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

140def no_fuel(+lo: Nat, +hi: Nat, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}, +hf: {Nat.is_le(Nat.sub(hi, lo), 0n) == True{} : Bool}) -> Empty:
141  N.lt_zero_absurd(0n, N.lt_le_trans(0n, Nat.sub(hi, lo), 0n, sub_pos(lo, hi, hlt), hf))

Uses (9)

Used by (1)