def not_lt_zero
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Natimport Base
86def not_lt_zero(+n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
87 match n:
88 case 0n:
89 {==}
90 case 1n+p:
91 {==}
Uses (3)
Used by (9)
- bend-collections-laws-math@1.0.0.0/proofs/lib/nat:lt_zero_absurd
- bend-collections-laws-math@1.0.0.0/proofs/lib/nat:le_not_lt
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/width:fits_lt
- bend-collections-laws-math@1.0.0.0/proofs/math/random/fround:lt0f
- bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire:min_succ
- …