F64addc.cmpv: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend as F64addc
Lines 61-66 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&start_line=61&end_line=66

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

def cmpv(+a: WU.U64, +b: WU.U64) -> {X.cmp(a, b) == Nat.cmp(SW.value(a), SW.value(b)) : Cmp}:
  l1 = WA.lt_value(a, b)
  q1 = WA.eq_value(a, b)
  +e1 = Equal.cong(Bool, Cmp, t => X.cmp_pick(t, X.eq(a, b)), X.lt(a, b), Nat.is_lt(SW.value(a), SW.value(b)), l1)
  +e2 = Equal.cong(Bool, Cmp, t => X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), t), X.eq(a, b), Nat.is_eq(SW.value(a), SW.value(b)), q1)
  Equal.trans(Cmp, X.cmp_pick(X.lt(a, b), X.eq(a, b)), X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), X.eq(a, b)), Nat.cmp(SW.value(a), SW.value(b)), e1, Equal.trans(Cmp, X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), X.eq(a, b)), X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), Nat.is_eq(SW.value(a), SW.value(b))), Nat.cmp(SW.value(a), SW.value(b)), e2, cp_c(SW.value(a), SW.value(b), Nat.cmp(SW.value(a), SW.value(b)), {==})))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  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.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&name=cp_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=eq_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=lt_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=cmp_pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=lt