Order.internal_nat_le_antisymm_eq: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/order.bend as Order
Lines 105-106 of bend-mathlib@0.8.1.0/order.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/order.bend&start_line=105&end_line=106

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

def internal_nat_le_antisymm_eq(+a: Nat, +b: Nat, ab: MNat.le(a, b), ba: MNat.le(b, a)) -> {a == b : Nat}:
  le_antisymm_eq(~Nat, ~Nat.is_le, ~MNat.le_antisymm, a, b, ab, ba)

Uses (5):
  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=bend-mathlib@0.8.1.0/nat.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_antisymm
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/order.bend&name=le_antisymm_eq