def ab_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:152

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64mont.bend as UM

152def ab_lt(+bp: Nat, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hb: {Nat.is_lt(b, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}:
153  UM.ab_lt(bp, a, b, ha, hb)