def sc_lt_cancel

bend-collections-laws-math@1.0.0.0 · proofs/lib/arith.bend:54

import Base

54def sc_lt_cancel(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
55  sc_lt_cancel_g(k, a, b, Nat.is_lt(a, b), {==}, h)