def bigcmp
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addg.bend:158
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as F64addg
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
158def 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}:
159 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), {==}))