def shift_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/arith.bend:150

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/logic.bend as L

150# shift(k, a) < shift(k, b): a < b
151def shift_cancel(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
152  cancel_c(k, a, b, h, L.bool_cases(Nat.is_lt(a, b)))