def lt_zero_absurd

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:93

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

93def lt_zero_absurd(+n: Nat, e: {Nat.is_lt(n, 0n) == True{} : Bool}) -> Empty:
94  L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(n, 0n), True{}, Equal.sym(Bool, Nat.is_lt(n, 0n), False{}, not_lt_zero(n)), e))