law lt_zero
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1572# No natural is less than zero.
1573law lt_zero:
1574 for n: Nat
1575 lt(n, 0n) -> Empty
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1572# No natural is less than zero.
1573law lt_zero:
1574 for n: Nat
1575 lt(n, 0n) -> Empty