def unfit_mul_r

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

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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

951def unfit_mul_r(+x: Nat, +y: Nat, +hy: {C.fits(32n, y) == False{} : Bool}, +hx: {Nat.is_le(1n, x) == True{} : Bool}) -> {C.fits(32n, Nat.mul(x, y)) == False{} : Bool}:
952  L.subst(Nat, z => {C.fits(32n, z) == False{} : Bool}, Nat.mul(y, x), Nat.mul(x, y), NA.mul_comm(y, x), unfit_mul(y, x, hy, hx))