def lt_hi

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

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
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

282# y1 < y2: x1 + shift(k, y1) < x2 + shift(k, y2)
283def lt_hi(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +h: {Nat.is_lt(y1, y2) == True{} : Bool}) -> {Nat.is_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == True{} : Bool}:
284  +h1 = L.subst(Nat, z => {Nat.is_lt(x1, z) == True{} : Bool}, C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k)), lt_of_fits(k, x1, hx1))
285  +h2 = N.lt_add_r2(x1, C.shift(k, 1n), C.shift(k, y1), h1)
286  +e2 = Equal.sym(Nat, C.shift(k, Nat.add(1n, y1)), Nat.add(C.shift(k, 1n), C.shift(k, y1)), shift_add(k, 1n, y1))
287  +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(x1, C.shift(k, y1)), z) == True{} : Bool}, Nat.add(C.shift(k, 1n), C.shift(k, y1)), C.shift(k, 1n+y1), e2, h2)
288  +h4 = shift_mono(k, 1n+y1, y2, N.lt_succ_le_succ(y1, y2, h))
289  +h5 = L.subst(Nat, z => {Nat.is_le(C.shift(k, y2), z) == True{} : Bool}, Nat.add(C.shift(k, y2), x2), Nat.add(x2, C.shift(k, y2)), N.add_comm(C.shift(k, y2), x2), N.le_add_right(C.shift(k, y2), x2))
290  N.lt_le_trans(Nat.add(x1, C.shift(k, y1)), C.shift(k, 1n+y1), Nat.add(x2, C.shift(k, y2)), h3, N.le_trans(C.shift(k, 1n+y1), C.shift(k, y2), Nat.add(x2, C.shift(k, y2)), h4, h5))