def lt_cancel_mul

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64div.bend:173

import Base

173def lt_cancel_mul(+a: Nat, +b: Nat, +d: Nat, +h: {Nat.is_lt(Nat.mul(a, d), Nat.mul(b, d)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
174  lt_cancel_mul_c(a, b, d, h, Nat.is_lt(a, b), {==})