def uint_trans

stelliferous@0.0.2.0 · proofs/nat_to_u32_bounds.bend:66

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

66def 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,
67    c) == True{} : Bool}:
68  %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}
69  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))