NatToU32Bounds.uint_trans: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as NatToU32Bounds
Lines 66-69 of stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&start_line=66&end_line=69

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison

def uint_trans(+a: U32,+b: U32,+c: U32,ab: {U32.is_lt(a,b) == True{} : Bool},bc: {U32.is_le(b,c) == True{} : Bool}) -> {U32.is_lt(a,
    c) == True{} : Bool}:
  %Equal.sym(Bool,U32.is_lt(a,c),Nat.is_lt(U32.to_nat(a),U32.to_nat(c)),Comparison.lt(a,c)) : {_ == True{} : Bool}
  nat_trans(U32.to_nat(a),U32.to_nat(b),U32.to_nat(c),as_nat_lt(a,b,ab),as_nat_le(b,c,bc))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=as_nat_le
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=as_nat_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=nat_trans
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=lt