def o48_shl_inv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:162

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

162def o48_shl_inv(+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}:
163  o48_shl_inv_c(k, a, b, h, Nat.is_lt(a, b), {==})