def sq_fits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:975

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

975def sq_fits(+more: Bool, +b: WU.U64, +bok: Bool, +nb: Nat, +md: Bool, +hB: {C.fits(64n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hm: {mode(md, nb) == True{} : Bool}) -> {C.fits(64n, NF.sqn(more, nb)) == G.sq_ok(~WU.U64, ~I.u64_is, more, b, bok) : Bool}:
976  match more bok:
977    case False{} _:
978      hB
979    case True{} True{}:
980      ok_mul(b, b, Nat.mul(nb, nb), nmul(v(b), v(b), nb, nb, hb, hb))
981    case True{} False{}:
982      +md1 = unfit_big(nb, md, hm, hB)
983      +h1 = L.subst(Bool, t => {mode(t, nb) == True{} : Bool}, md, True{}, md1, hm)
984      unfit_mul(nb, nb, hB, h1)