def gcmp_lt

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

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/lib/nat.bend as N

62def gcmp_lt(+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, +c2: Nat, +hc2: {c2 == 1n : Nat}, +F2: Nat, +hlt: {Nat.is_lt(E1, E2) == True{} : Bool}) -> {Nat.is_lt(C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1))), C.shift(SF.pick(Nat, False{}, 1n, E2), Nat.add(F2, C.shift(52n, c2)))) == True{} : Bool}:
63  +G1 = C.shift(SF.pick(Nat, b1, 1n, E1), Nat.add(F1, C.shift(52n, c1)))
64  +G2 = C.shift(E2, Nat.add(F2, C.shift(52n, c2)))
65  +ha = gub(one, h1, E1, b1, hb1, c1, hc1, F1, hF1)
66  +hb = shmk(1n+E1, E2, C.shift(52n, one), N.lt_succ_le_succ(E1, E2, hlt))
67  +hc = glb(one, h1, E2, c2, hc2, F2)
68  N.lt_le_trans(G1, C.shift(1n+E1, C.shift(52n, one)), G2, ha, N.le_trans(C.shift(1n+E1, C.shift(52n, one)), C.shift(E2, C.shift(52n, one)), G2, hb, hc))