U32half.sub_bridge: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as U32half
Lines 154-168 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend&start_line=154&end_line=168

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

def sub_bridge(+a: Nat, +b: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +ha: {Nat.is_lt(a, SC.pow2(k)) == True{} : Bool}, +hb: {Nat.is_le(b, a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a), U32.from_nat(b)) == U32.from_nat(Nat.sub(a, b)) : U32}:
  +hb2 = N.le_lt_trans(b, a, SC.pow2(k), hb, ha)
  +ra = U.to_nat_from_nat(a, k, hk, ha)
  +rb = U.to_nat_from_nat(b, k, hk, hb2)
  +le = L.subst(Nat, z => {Nat.is_le(z, U32.to_nat(U32.from_nat(a))) == True{} : Bool}, b, U32.to_nat(U32.from_nat(b)), Equal.sym(Nat, U32.to_nat(U32.from_nat(b)), b, rb),
          L.subst(Nat, z => {Nat.is_le(b, z) == True{} : Bool}, a, U32.to_nat(U32.from_nat(a)), Equal.sym(Nat, U32.to_nat(U32.from_nat(a)), a, ra), hb))
  U.injective(U32.sub(U32.from_nat(a), U32.from_nat(b)), U32.from_nat(Nat.sub(a, b)),
    Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(a), U32.from_nat(b))), Nat.sub(a, b), U32.to_nat(U32.from_nat(Nat.sub(a, b))),
      Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(a), U32.from_nat(b))), Nat.sub(U32.to_nat(U32.from_nat(a)), U32.to_nat(U32.from_nat(b))), Nat.sub(a, b),
        U.sub_nat(U32.from_nat(a), U32.from_nat(b), le),
        Equal.trans(Nat, Nat.sub(U32.to_nat(U32.from_nat(a)), U32.to_nat(U32.from_nat(b))), Nat.sub(a, U32.to_nat(U32.from_nat(b))), Nat.sub(a, b),
          Equal.cong(Nat, Nat, z => Nat.sub(z, U32.to_nat(U32.from_nat(b))), U32.to_nat(U32.from_nat(a)), a, ra),
          Equal.cong(Nat, Nat, z => Nat.sub(a, z), U32.to_nat(U32.from_nat(b)), b, rb))),
      Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.sub(a, b))), Nat.sub(a, b),
        U.to_nat_from_nat(Nat.sub(a, b), k, hk, N.le_lt_trans(Nat.sub(a, b), a, SC.pow2(k), sub_le(a, b), ha)))))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=injective
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=sub_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=to_nat_from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend&name=sub_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2