def shift_mono

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:191

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

191def shift_mono(+k: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(C.shift(k, x), C.shift(k, y)) == True{} : Bool}:
192  match k:
193    case 0n:
194      h
195    case 1n+ +p:
196      N.double_le(C.shift(p, x), C.shift(p, y), shift_mono(p, x, y, h))