def lt_sh2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:65

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/math/typed/width.bend as WW

65def lt_sh2(+j: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(C.shift(j, C.shift(j, a)), C.shift(j, C.shift(j, b))) == True{} : Bool}:
66  WW.shift_lt(j, C.shift(j, a), C.shift(j, b), WW.shift_lt(j, a, b, h))