def le_cancel

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/combnat.bend:36

import Base

36def le_cancel(+a: Nat, +b: Nat, +cp: Nat, +h: {Nat.is_le(Nat.mul(a, 1n+cp), Nat.mul(b, 1n+cp)) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
37  le_cancel_c(a, b, cp, h, Nat.is_lt(b, a), {==})