def sc_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/arith.bend:40

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

40def sc_lt(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool}:
41  match k:
42    case 0n:
43      h
44    case 1n+j:
45      N.double_lt(sc(j, a), sc(j, b), sc_lt(j, a, b, h))