def unfit_mul

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

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/proofs/math/natural/roots.bend as RT

947# x unfit, 1 <= y: x y unfit
948def unfit_mul(+x: Nat, +y: Nat, +hx: {C.fits(32n, x) == False{} : Bool}, +hy: {Nat.is_le(1n, y) == True{} : Bool}) -> {C.fits(32n, Nat.mul(x, y)) == False{} : Bool}:
949  unfit_mono(32n, x, Nat.mul(x, y), RT.le_mul_pos(x, y, pos_of(y, hy)), hx)