F64addg.bigcmp: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as F64addg
Lines 158-159 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&start_line=158&end_line=159

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

def bigcmp(+one: Nat, +h1: {one == 1n : Nat}, +el: Nat, +es: Nat, +Fl: Nat, +Fs: Nat, +hFl: {C.fits(52n, Fl) == True{} : Bool}, +hFs: {C.fits(52n, Fs) == True{} : Bool}, +hlt: {Nat.is_lt(es, el) == True{} : Bool}) -> {Nat.cmp(mt(es, Fs), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == LT{} : Cmp}:
  NC.cmp_lt(mt(es, Fs), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), bigcmp_c(one, h1, el, es, Fl, Fs, hFl, hFs, hlt, Nat.is_eq(es, 0n), {==}))

Uses (13):
  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=Nat
  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=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=bigcmp_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=mt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=xe
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=cmp_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift