~/jendhub

law lt_asymm

bend-mathlib@0.8.1.0 · nat.bend:2612

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

2612# The strict order is asymmetric: a < b rules out b < a.
2613law lt_asymm:
2614  for a: Nat
2615  for b: Nat
2616  for h: lt(a, b)
2617  lt(b, a) -> Empty

Uses (5)

Used by (0)

No other definition uses this definition.