~/jendhub

def internal_nat_le_total_true

bend-mathlib@0.8.1.0 · order.bend:108

import bend-mathlib@0.8.1.0/order.bend as Order
import Base

108def internal_nat_le_total_true(+a: Nat, +b: Nat) -> {Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) == True{} : Bool}:
109  le_total_true(~Nat, ~Nat.is_le, ~internal_nat_le_total, a, b)

Uses (6)

Used by (0)

No other definition uses this definition.