def sq_fits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:974

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/proofs/math/typed/natfuel.bend as NF

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