def gcmp

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:96

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

96def gcmp(+one: Nat, +h1: {one == 1n : Nat}, +E1: Nat, +b1: Bool, +hb1: {Nat.is_eq(E1, 0n) == b1 : Bool}, +c1: Nat, +hc1: {c1 == SF.b2n(Bool.not(b1)) : Nat}, +F1: Nat, +hF1: {C.fits(52n, F1) == True{} : Bool}, +E2: Nat, +b2: Bool, +hb2: {Nat.is_eq(E2, 0n) == b2 : Bool}, +c2: Nat, +hc2: {c2 == SF.b2n(Bool.not(b2)) : Nat}, +F2: Nat, +hF2: {C.fits(52n, F2) == True{} : Bool}) -> {Nat.cmp(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, b2, 1n, E2), Nat.add(F2, C.shift(52n, c2)))) == NC.lex(Nat.cmp(E1, E2), Nat.cmp(F1, F2)) : Cmp}:
97  gcmp_c(one, h1, E1, b1, hb1, c1, hc1, F1, hF1, E2, b2, hb2, c2, hc2, F2, hF2, Nat.cmp(E1, E2), {==})