def lt_zero_false

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32.bend:116

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32
import Base

116def lt_zero_false(+n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
117  match n:
118    case 0n:
119      {==}
120    case 1n+p:
121      {==}

Uses (3)

Used by (2)