def ilog_done

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/logs.bend:78

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

78def ilog_done(+np: Nat, +bq: Nat) -> {M.ilog(1n+np, 2n+bq) == Done{ilog_value(np, bq)} : Result<&2, &2, M.MathError, Nat>}:
79  %Equal.sym(Bool, Nat.is_lt(2n+bq, 2n), False{}, lt_two(bq)) : {M.ilog_ok(1n+np, 2n+bq, Bool.or(False{}, _)) == Done{ilog_value(np, bq)} : Result<&2, &2, M.MathError, Nat>}
80  {==}