def internal_nat_le_antisymm_eq

bend-mathlib@0.8.1.0 · order.bend:105

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

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