def unfit_mul

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

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

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