U32.internal_max_fin: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 757-762 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=757&end_line=762

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

def internal_max_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, v, u)) == Nat.max(U32.to_nat(u), U32.to_nat(v)) : Nat}:
  match c:
    case True{}:
      Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.max_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
    case False{}:
      Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.max_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  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
  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.max
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_of_not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=max_eq_left
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=max_eq_right