def ilends

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:265

import Base

265def ilends(f: Nat, +q: Nat, +b: Nat, +p: Nat, +up: Bool) -> Bool:
266  match f up:
267    case 0n False{}:
268      True{}
269    case 0n True{}:
270      False{}
271    case 1n+g False{}:
272      True{}
273    case 1n+g True{}:
274      ilends(g, q, b, Nat.mul(p, b), Nat.is_le(Nat.mul(p, b), q))