F64cmp.nl: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as F64cmp
Lines 168-176 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&start_line=168&end_line=176

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

# neither infinite nor NaN: the exponent field is not 2047
def nl(+a: Bool, +d: Bool, +hi: {Bool.and(a, d) == False{} : Bool}, +hn: {Bool.and(a, Bool.not(d)) == False{} : Bool}) -> {a == False{} : Bool}:
  match a d:
    case True{} True{}:
      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, hi))
    case True{} False{}:
      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, hn))
    case False{} _:
      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=absurd_tf