def sc_le

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

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

33def sc_le(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(sc(k, a), sc(k, b)) == True{} : Bool}:
34  match k:
35    case 0n:
36      h
37    case 1n+j:
38      N.double_le(sc(j, a), sc(j, b), sc_le(j, a, b, h))