F64cmp.eqs: 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 293-302 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=293&end_line=302

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U

def eqs(+eL: Bool, +eW: Bool, +sa: Bool, +sb: Bool, +mc: Cmp, +h: {Bool.and(eL, eW) == Cmp.is_eq(mc) : Bool}) -> {Bool.and(eL, Bool.and(eW, Nat.is_eq(SF.b2n(sa), SF.b2n(sb)))) == Cmp.is_eq(SF.pick(Cmp, Bool.not(Bool.xor(sa, sb)), SF.pick(Cmp, sa, SF.flip(mc), mc), SF.pick(Cmp, sa, LT{}, GT{}))) : Bool}:
  match sa sb:
    case True{} True{}:
      Equal.trans(Bool, Bool.and(eL, Bool.and(eW, True{})), Bool.and(eL, eW), Cmp.is_eq(SF.flip(mc)), Equal.cong(Bool, Bool, t => Bool.and(eL, t), Bool.and(eW, True{}), eW, U.and_true(eW)), Equal.trans(Bool, Bool.and(eL, eW), Cmp.is_eq(mc), Cmp.is_eq(SF.flip(mc)), h, eqflip(mc)))
    case False{} False{}:
      Equal.trans(Bool, Bool.and(eL, Bool.and(eW, True{})), Bool.and(eL, eW), Cmp.is_eq(mc), Equal.cong(Bool, Bool, t => Bool.and(eL, t), Bool.and(eW, True{}), eW, U.and_true(eW)), h)
    case True{} False{}:
      andff(eL, eW)
    case False{} True{}:
      andff(eL, eW)

Uses (15):
  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=Bool.xor
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=and_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=andff
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=eqflip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=flip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick