law lt_irrefl
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
484# No natural is less than itself.
485law lt_irrefl:
486 for a: Nat
487 lt(a, a) -> Empty
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
484# No natural is less than itself.
485law lt_irrefl:
486 for a: Nat
487 lt(a, a) -> Empty