~/jendhub

def internal_nat_le_total_true_sym

bend-mathlib@0.8.1.0 · order.bend:128

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

128# Calls of the twins, as the calls above the generated section make of their laws (PLAN F38).
129def internal_nat_le_total_true_sym(+a: Nat, +b: Nat) -> {True{} == Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) : Bool}:
130  le_total_true_sym(~Nat, ~Nat.is_le, ~internal_nat_le_total, a, b)

Uses (6)

Used by (0)

No other definition uses this definition.