def sc16_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:242

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR

242# 2^16 x < 2^32 for x < 2^16
243def sc16_lt(+one: Nat, +x: Nat, +hx: {Nat.is_lt(x, WD.sc(16n, one)) == True{} : Bool}) -> {Nat.is_lt(WD.sc(16n, x), WD.sc(32n, one)) == True{} : Bool}:
244  L.subst(Nat, z => {Nat.is_lt(WD.sc(16n, x), z) == True{} : Bool}, WD.sc(16n, WD.sc(16n, one)), WD.sc(32n, one), sc_sc(16n, 16n, one), AR.sc_lt(16n, x, WD.sc(16n, one), hx))