~/jendhub

def shift_ge

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

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as Width
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

240def shift_ge(+k: Nat, +x: Nat) -> {Nat.is_le(x, C.shift(k, x)) == True{} : Bool}:
241  match k:
242    case 0n:
243      N.le_refl(x)
244    case 1n+ +p:
245      N.le_trans(x, C.shift(p, x), Nat.double(C.shift(p, x)), shift_ge(p, x), N.double_self_le(C.shift(p, x)))

Uses (8)

Used by (16)