import Base
import ./f64light.bend as FL
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./natcmp.bend as NC
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64round.bend as FR
import ./f64mexp.bend as EX
import ./f64divf.bend as DF
import ./f64divx.bend as DX

# Div.value, the finite nonzero case: SoftFloat's f64_div on the normalized
# significands (div_n) is the spec's div_fin.

def v(+x: U32) -> Nat:
  U32.to_nat(x)

def pos52(+n: Nat, +h: {C.fits(52n, n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
  match n:
    case 0n:
      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
    case 1n+ +np:
      N.zero_le(np)

def hi_nz_c(+l: U32, +h: U32, +hf: {C.fits(32n, SW.value(WU.U64{l, h})) == False{} : Bool}, +z: Bool, +hz: {Nat.is_eq(v(h), 0n) == z : Bool}) -> {z == False{} : Bool}:
  match z:
    case True{}:
      +e0 = N.eq_from_is_eq(v(h), 0n, hz)
      +e1 = Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), C.shift(32n, 0n)), v(l), Equal.cong(Nat, Nat, w => Nat.add(v(l), C.shift(32n, w)), v(h), 0n, e0), N.add_zero(v(l)))
      +f1 = L.subst(Nat, w => {C.fits(32n, w) == True{} : Bool}, v(l), SW.value(WU.U64{l, h}), Equal.sym(Nat, SW.value(WU.U64{l, h}), v(l), e1), LW.vb(l))
      Equal.trans(Bool, True{}, C.fits(32n, SW.value(WU.U64{l, h})), False{}, Equal.sym(Bool, C.fits(32n, SW.value(WU.U64{l, h})), True{}, f1), hf)
    case False{}:
      {==}

def hi_nz(+b: WU.U64, +hf: {C.fits(32n, SW.value(b)) == False{} : Bool}) -> {U32.is_zero(X.hi(b)) == False{} : Bool}:
  match b:
    case WU.U64{+l, +h}:
      Equal.trans(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), False{}, LW.zero_nat(h), hi_nz_c(l, h, hf, Nat.is_eq(v(h), 0n), {==}))

# b <= a and a < 2 b give a - b < b
def sub_lt_of(+a: Nat, +b: Nat, +hle: {Nat.is_le(b, a) == True{} : Bool}, +h: {Nat.is_lt(a, Nat.add(b, b)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, b), b) == True{} : Bool}:
  +e = N.sub_add(a, b, hle)
  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(b, b)) == True{} : Bool}, a, Nat.add(b, Nat.sub(a, b)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, e), h)
  Equal.trans(Bool, Nat.is_lt(Nat.sub(a, b), b), Nat.is_lt(Nat.add(b, Nat.sub(a, b)), Nat.add(b, b)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(b, Nat.sub(a, b)), Nat.add(b, b)), Nat.is_lt(Nat.sub(a, b), b), WW.lt_cancel_l(b, Nat.sub(a, b), b)), h2)

def sub_le0(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+ +bp:
      {==}
    case 1n+ +ap 0n:
      N.le_refl(1n+ap)
    case 1n+ +ap 1n+ +bp:
      N.le_trans(Nat.sub(ap, bp), ap, 1n+ap, sub_le0(ap, bp), N.le_succ(ap))

def add_lt2(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, a), Nat.add(b, b)) == True{} : Bool}:
  FL.add_lt2(a, b, h)

# a normalized significand is in [2^52, 2^53)
def lo52(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +h: {C.fits(52n, n) == False{} : Bool}) -> {Nat.is_le(C.shift(52n, one), n) == True{} : Bool}:
  N.not_lt_le(n, C.shift(52n, one), Equal.trans(Bool, Nat.is_lt(n, C.shift(52n, one)), C.fits(52n, n), False{}, FR.lt_fit(52n, one, h1, n), h))

def hi53(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +h: {C.fits(53n, n) == True{} : Bool}) -> {Nat.is_lt(n, C.shift(53n, one)) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_lt(n, C.shift(53n, one)), C.fits(53n, n), True{}, FR.lt_fit(53n, one, h1, n), h)

# 2^53 <= 2 n and n < 2 m for normalized n, m
def dbl53(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +h: {C.fits(52n, n) == False{} : Bool}) -> {Nat.is_le(C.shift(53n, one), Nat.add(n, n)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_le(C.shift(53n, one), z) == True{} : Bool}, Nat.double(n), Nat.add(n, n), NA.double_self(n), N.double_le(C.shift(52n, one), n, lo52(one, h1, n, h)))

def lt2x(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +m: Nat, +hn: {C.fits(53n, n) == True{} : Bool}, +hm: {C.fits(52n, m) == False{} : Bool}) -> {Nat.is_lt(n, Nat.add(m, m)) == True{} : Bool}:
  N.lt_le_trans(n, C.shift(53n, one), Nat.add(m, m), hi53(one, h1, n, hn), dbl53(one, h1, m, hm))

def dq_lt(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +EA: Nat, +A: WU.U64, +EB: Nat, +B: WU.U64, +MX: Nat, +yp: Nat, +sx: Nat, +sy: Nat, +XX: Nat, +XY: Nat, +hA: {SW.value(A) == C.shift(sx, MX) : Nat}, +hB: {SW.value(B) == C.shift(sy, 1n+yp) : Nat}, +a53: {C.fits(53n, SW.value(A)) == True{} : Bool}, +a52: {C.fits(52n, SW.value(A)) == False{} : Bool}, +b53: {C.fits(53n, SW.value(B)) == True{} : Bool}, +b52: {C.fits(52n, SW.value(B)) == False{} : Bool}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hsx: {Nat.is_le(sx, 53n) == True{} : Bool}, +hsy: {Nat.is_le(sy, 53n) == True{} : Bool}, +hXX: {Nat.is_le(1926n, XX) == True{} : Bool}, +hXY: {Nat.is_le(XY, 3971n) == True{} : Bool}, +hlt0: {Nat.is_lt(SW.value(A), SW.value(B)) == True{} : Bool}) -> {F.div_q(s, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), X.add(A, A), B) == SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : F.F64}:
  +hlt = hlt0
  +hu2 = N.le_trans(Nat.add(62n, 1n+sx), Nat.add(62n, 54n), 200n, N.le_add_left(1n+sx, 54n, 62n, hsx), {==})
  +hva = Equal.trans(Nat, SW.value(X.add(A, A)), C.low(64n, Nat.add(SW.value(A), SW.value(A))), C.shift(1n+sx, MX), WA.add_value(A, A), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(A), SW.value(A))), Nat.add(SW.value(A), SW.value(A)), C.shift(1n+sx, MX), WW.low_fit(64n, Nat.add(SW.value(A), SW.value(A)), SH.fits_mono(54n, 64n, Nat.add(SW.value(A), SW.value(A)), {==}, FR.fits_add1(53n, SW.value(A), SW.value(A), a53, a53))), Equal.trans(Nat, Nat.add(SW.value(A), SW.value(A)), Nat.double(SW.value(A)), C.shift(1n+sx, MX), Equal.sym(Nat, Nat.double(SW.value(A)), Nat.add(SW.value(A), SW.value(A)), NA.double_self(SW.value(A))), Equal.cong(Nat, Nat, z => Nat.double(z), SW.value(A), C.shift(sx, MX), hA))))
  +hle = L.subst(Nat, z => {Nat.is_le(SW.value(B), z) == True{} : Bool}, Nat.add(SW.value(A), SW.value(A)), SW.value(X.add(A, A)), Equal.sym(Nat, SW.value(X.add(A, A)), Nat.add(SW.value(A), SW.value(A)), Equal.trans(Nat, SW.value(X.add(A, A)), C.low(64n, Nat.add(SW.value(A), SW.value(A))), Nat.add(SW.value(A), SW.value(A)), WA.add_value(A, A), WW.low_fit(64n, Nat.add(SW.value(A), SW.value(A)), SH.fits_mono(54n, 64n, Nat.add(SW.value(A), SW.value(A)), {==}, FR.fits_add1(53n, SW.value(A), SW.value(A), a53, a53))))), N.lt_le(SW.value(B), Nat.add(SW.value(A), SW.value(A)), lt2x(one, h1, SW.value(B), SW.value(A), b53, a52)))
  +hRlt = L.subst(Nat, z => {Nat.is_lt(Nat.sub(z, SW.value(B)), SW.value(B)) == True{} : Bool}, Nat.add(SW.value(A), SW.value(A)), SW.value(X.add(A, A)), Equal.sym(Nat, SW.value(X.add(A, A)), Nat.add(SW.value(A), SW.value(A)), Equal.trans(Nat, SW.value(X.add(A, A)), C.low(64n, Nat.add(SW.value(A), SW.value(A))), Nat.add(SW.value(A), SW.value(A)), WA.add_value(A, A), WW.low_fit(64n, Nat.add(SW.value(A), SW.value(A)), SH.fits_mono(54n, 64n, Nat.add(SW.value(A), SW.value(A)), {==}, FR.fits_add1(53n, SW.value(A), SW.value(A), a53, a53))))), sub_lt_of(Nat.add(SW.value(A), SW.value(A)), SW.value(B), N.lt_le(SW.value(B), Nat.add(SW.value(A), SW.value(A)), lt2x(one, h1, SW.value(B), SW.value(A), b53, a52)), add_lt2(SW.value(A), SW.value(B), hlt)))
  +hf = Equal.trans(Nat, Nat.add(Nat.add(1n, sx), 1021n), Nat.add(sx, 1022n), Nat.add(sx, 1022n), Equal.trans(Nat, Nat.add(Nat.add(1n, sx), 1021n), Nat.add(Nat.add(sx, 1n), 1021n), Nat.add(sx, 1022n), Equal.cong(Nat, Nat, z => Nat.add(z, 1021n), Nat.add(1n, sx), Nat.add(sx, 1n), Equal.trans(Nat, Nat.add(1n, sx), Nat.add(1n, Nat.add(sx, 0n)), Nat.add(sx, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.trans(Nat, Nat.add(1n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(1n, 0n)), Nat.add(sx, 1n), NA.add_swap(1n, sx, 0n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(sx, 1n), 1021n), Nat.add(sx, Nat.add(1n, 1021n)), Nat.add(sx, 1022n), NA.add_assoc(sx, 1n, 1021n), {==})), Equal.sym(Nat, Nat.add(sx, 1022n), Nat.add(sx, 1022n), Equal.trans(Nat, Nat.add(sx, 1022n), Nat.add(Nat.add(sx, 0n), 1022n), Nat.add(sx, 1022n), Equal.cong(Nat, Nat, z => Nat.add(z, 1022n), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), 1022n), Nat.add(sx, Nat.add(0n, 1022n)), Nat.add(sx, 1022n), NA.add_assoc(sx, 0n, 1022n), {==}))))
  +hu = N.le_trans(sy, 62n, Nat.add(62n, 1n+sx), N.le_trans(sy, 53n, 62n, hsy, {==}), N.le_add_right(62n, 1n+sx))
  +hP = Equal.sym(Nat, Nat.add(sy, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.add(62n, 1n+sx), N.sub_add(Nat.add(62n, 1n+sx), sy, hu))
  +hP200 = N.le_trans(Nat.sub(Nat.add(62n, 1n+sx), sy), Nat.add(62n, 1n+sx), 200n, sub_le0(Nat.add(62n, 1n+sx), sy), hu2)
  +hdp = Equal.trans(Nat, Nat.add(Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.add(Nat.sub(Nat.add(62n, 1n+sx), sy), Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy))), 200n, NA.add_comm(Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.sub(Nat.add(62n, 1n+sx), sy)), N.sub_add(200n, Nat.sub(Nat.add(62n, 1n+sx), sy), hP200))
  +bp = Nat.sub(SW.value(B), 1n)
  +hBp = Equal.sym(Nat, 1n+Nat.sub(SW.value(B), 1n), SW.value(B), N.sub_add(SW.value(B), 1n, pos52(SW.value(B), b52)))
  +hhi = hi_nz(B, DF.nfit_mono(32n, 52n, SW.value(B), {==}, b52))
  +eEA = EX.eg(EA, sx, XX, hEAx, hsx, hXX)
  +hEB = N.le_trans(EB, Nat.add(EB, sy), 6142n, N.le_add_right(EB, sy), L.subst(Nat, z => {Nat.is_le(z, 6142n) == True{} : Bool}, Nat.add(XY, 2171n), Nat.add(EB, sy), Equal.sym(Nat, Nat.add(EB, sy), Nat.add(XY, 2171n), hEBy), Equal.trans(Bool, Nat.is_le(Nat.add(XY, 2171n), Nat.add(3971n, 2171n)), Nat.is_le(XY, 3971n), True{}, FR.le_cancel_r(XY, 3971n, 2171n), hXY)))
  +hEA2 = Equal.trans(Bool, Nat.is_le(Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(EA, Nat.add(F.off(), 1021n))), Nat.is_le(4044n, EA), True{}, FR.le_cancel_r(4044n, EA, Nat.add(F.off(), 1021n)), eEA)
  +hle2 = N.le_trans(EB, 6142n, Nat.add(EA, Nat.add(F.off(), 1021n)), hEB, N.le_trans(6142n, Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(EA, Nat.add(F.off(), 1021n)), {==}, hEA2))
  +hd = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Nat.add(EB, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB)), Nat.add(EA, Nat.add(F.off(), 1021n)), NA.add_comm(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), N.sub_add(Nat.add(EA, Nat.add(F.off(), 1021n)), EB, hle2))
  +he1 = L.subst(Nat, z => {Nat.is_le(Nat.add(4044n, Nat.add(F.off(), 1021n)), z) == True{} : Bool}, Nat.add(EA, Nat.add(F.off(), 1021n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Nat.add(EA, Nat.add(F.off(), 1021n)), hd), hEA2)
  +he2 = N.le_trans(Nat.add(2180n, 6142n), Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n), {==}, N.le_trans(Nat.add(4044n, Nat.add(F.off(), 1021n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), EB), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n), he1, N.le_add_left(EB, 6142n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), hEB)))
  +he = Equal.trans(Bool, Nat.is_le(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB)), Nat.is_le(Nat.add(2180n, 6142n), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(2180n, 6142n), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n)), Nat.is_le(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB)), FR.le_cancel_r(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 6142n)), he2)
  +hx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), NA.add_comm(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), 2180n), N.sub_add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n, he))
  +hXl = Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(XY, 200n), 1n), Nat.add(3971n, 201n)), Nat.is_le(Nat.add(XY, 201n), Nat.add(3971n, 201n)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(3971n, 201n)), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(XY, 200n), Nat.add(XY, 200n), Equal.trans(Nat, Nat.add(XY, 200n), Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, 200n), Equal.cong(Nat, Nat, z => Nat.add(z, 200n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, Nat.add(0n, 200n)), Nat.add(XY, 200n), NA.add_assoc(XY, 0n, 200n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, Nat.add(200n, 1n)), Nat.add(XY, 201n), NA.add_assoc(XY, 200n, 1n), {==})), Equal.sym(Nat, Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==}))))), Equal.trans(Bool, Nat.is_le(Nat.add(XY, 201n), Nat.add(3971n, 201n)), Nat.is_le(XY, 3971n), True{}, FR.le_cancel_r(XY, 3971n, 201n), hXY))
  +hXx = Equal.trans(Bool, Nat.is_le(Nat.add(1926n, 3000n), Nat.add(XX, 3000n)), Nat.is_le(1926n, XX), True{}, FR.le_cancel_r(1926n, XX, 3000n), hXX)
  +hXle = N.le_trans(Nat.add(Nat.add(XY, 200n), 1n), 4926n, Nat.add(XX, 3000n), N.le_trans(Nat.add(Nat.add(XY, 200n), 1n), 4172n, 4926n, hXl, {==}), hXx)
  +ha = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(XY, 201n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), N.add_zero(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), z), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(0n, Nat.add(XY, 201n))), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), NA.add_assoc(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n, Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), z), Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_swap(0n, XY, 201n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(XY, 200n), Nat.add(XY, 200n), Equal.trans(Nat, Nat.add(XY, 200n), Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, 200n), Equal.cong(Nat, Nat, z => Nat.add(z, 200n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, Nat.add(0n, 200n)), Nat.add(XY, 200n), NA.add_assoc(XY, 0n, 200n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, Nat.add(200n, 1n)), Nat.add(XY, 201n), NA.add_assoc(XY, 200n, 1n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XY, 201n), z), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), N.add_zero(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)))))), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(XY, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(XY, Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n))), Nat.add(XY, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n)), NA.add_assoc(XY, 201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Equal.cong(Nat, Nat, z => Nat.add(XY, z), Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n), Equal.trans(Nat, Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(201n, 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n), NA.add_swap(201n, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), {==}))), NA.add_swap(XY, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n))))), N.sub_add(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n), hXle))
  +hG = DX.dexp(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), XX, XY, Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), Nat.sub(Nat.add(62n, 1n+sx), sy), 1n+sx, 1021n, sx, sy, EA, EB, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), ha, hdp, hP, hf, hEAx, hEBy, hd)
  +hEx = NR.add_cancel(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy))), Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), Equal.trans(Nat, Nat.add(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)))), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Equal.trans(Nat, Nat.add(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)))), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy))), 2180n), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), NA.add_comm(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)))), hG), Equal.sym(Nat, Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), Equal.trans(Nat, Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), Nat.add(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), 2180n), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), NA.add_comm(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n)), hx))))
  DF.dgen(one, h1, s, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1021n)), EB), 2180n), hx, X.add(A, A), B, Nat.sub(SW.value(B), 1n), hBp, MX, yp, 1n+sx, sy, Nat.sub(Nat.add(62n, 1n+sx), sy), Nat.sub(200n, Nat.sub(Nat.add(62n, 1n+sx), sy)), hva, hB, hP, hdp, hle, hRlt, hhi, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), hEx)

def dq_ge(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +EA: Nat, +A: WU.U64, +EB: Nat, +B: WU.U64, +MX: Nat, +yp: Nat, +sx: Nat, +sy: Nat, +XX: Nat, +XY: Nat, +hA: {SW.value(A) == C.shift(sx, MX) : Nat}, +hB: {SW.value(B) == C.shift(sy, 1n+yp) : Nat}, +a53: {C.fits(53n, SW.value(A)) == True{} : Bool}, +a52: {C.fits(52n, SW.value(A)) == False{} : Bool}, +b53: {C.fits(53n, SW.value(B)) == True{} : Bool}, +b52: {C.fits(52n, SW.value(B)) == False{} : Bool}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hsx: {Nat.is_le(sx, 53n) == True{} : Bool}, +hsy: {Nat.is_le(sy, 53n) == True{} : Bool}, +hXX: {Nat.is_le(1926n, XX) == True{} : Bool}, +hXY: {Nat.is_le(XY, 3971n) == True{} : Bool}, +hge0: {Nat.is_lt(SW.value(A), SW.value(B)) == False{} : Bool}) -> {F.div_q(s, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), A, B) == SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : F.F64}:
  +hge = hge0
  +hu2 = N.le_trans(Nat.add(62n, sx), Nat.add(62n, 54n), 200n, N.le_add_left(sx, 54n, 62n, N.le_trans(sx, 53n, 54n, hsx, {==})), {==})
  +hva = hA
  +hle = N.not_lt_le(SW.value(A), SW.value(B), hge)
  +hRlt = sub_lt_of(SW.value(A), SW.value(B), N.not_lt_le(SW.value(A), SW.value(B), hge), lt2x(one, h1, SW.value(A), SW.value(B), a53, b52))
  +hf = Equal.trans(Nat, Nat.add(sx, 1022n), Nat.add(sx, 1022n), Nat.add(sx, 1022n), {==}, {==})
  +hu = N.le_trans(sy, 62n, Nat.add(62n, sx), N.le_trans(sy, 53n, 62n, hsy, {==}), N.le_add_right(62n, sx))
  +hP = Equal.sym(Nat, Nat.add(sy, Nat.sub(Nat.add(62n, sx), sy)), Nat.add(62n, sx), N.sub_add(Nat.add(62n, sx), sy, hu))
  +hP200 = N.le_trans(Nat.sub(Nat.add(62n, sx), sy), Nat.add(62n, sx), 200n, sub_le0(Nat.add(62n, sx), sy), hu2)
  +hdp = Equal.trans(Nat, Nat.add(Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)), Nat.sub(Nat.add(62n, sx), sy)), Nat.add(Nat.sub(Nat.add(62n, sx), sy), Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy))), 200n, NA.add_comm(Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)), Nat.sub(Nat.add(62n, sx), sy)), N.sub_add(200n, Nat.sub(Nat.add(62n, sx), sy), hP200))
  +bp = Nat.sub(SW.value(B), 1n)
  +hBp = Equal.sym(Nat, 1n+Nat.sub(SW.value(B), 1n), SW.value(B), N.sub_add(SW.value(B), 1n, pos52(SW.value(B), b52)))
  +hhi = hi_nz(B, DF.nfit_mono(32n, 52n, SW.value(B), {==}, b52))
  +eEA = EX.eg(EA, sx, XX, hEAx, hsx, hXX)
  +hEB = N.le_trans(EB, Nat.add(EB, sy), 6142n, N.le_add_right(EB, sy), L.subst(Nat, z => {Nat.is_le(z, 6142n) == True{} : Bool}, Nat.add(XY, 2171n), Nat.add(EB, sy), Equal.sym(Nat, Nat.add(EB, sy), Nat.add(XY, 2171n), hEBy), Equal.trans(Bool, Nat.is_le(Nat.add(XY, 2171n), Nat.add(3971n, 2171n)), Nat.is_le(XY, 3971n), True{}, FR.le_cancel_r(XY, 3971n, 2171n), hXY)))
  +hEA2 = Equal.trans(Bool, Nat.is_le(Nat.add(4044n, Nat.add(F.off(), 1022n)), Nat.add(EA, Nat.add(F.off(), 1022n))), Nat.is_le(4044n, EA), True{}, FR.le_cancel_r(4044n, EA, Nat.add(F.off(), 1022n)), eEA)
  +hle2 = N.le_trans(EB, 6142n, Nat.add(EA, Nat.add(F.off(), 1022n)), hEB, N.le_trans(6142n, Nat.add(4044n, Nat.add(F.off(), 1022n)), Nat.add(EA, Nat.add(F.off(), 1022n)), {==}, hEA2))
  +hd = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), EB), Nat.add(EB, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB)), Nat.add(EA, Nat.add(F.off(), 1022n)), NA.add_comm(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), EB), N.sub_add(Nat.add(EA, Nat.add(F.off(), 1022n)), EB, hle2))
  +he1 = L.subst(Nat, z => {Nat.is_le(Nat.add(4044n, Nat.add(F.off(), 1022n)), z) == True{} : Bool}, Nat.add(EA, Nat.add(F.off(), 1022n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), EB), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), EB), Nat.add(EA, Nat.add(F.off(), 1022n)), hd), hEA2)
  +he2 = N.le_trans(Nat.add(2180n, 6142n), Nat.add(4044n, Nat.add(F.off(), 1022n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 6142n), {==}, N.le_trans(Nat.add(4044n, Nat.add(F.off(), 1022n)), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), EB), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 6142n), he1, N.le_add_left(EB, 6142n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), hEB)))
  +he = Equal.trans(Bool, Nat.is_le(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB)), Nat.is_le(Nat.add(2180n, 6142n), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 6142n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(2180n, 6142n), Nat.add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 6142n)), Nat.is_le(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB)), FR.le_cancel_r(2180n, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 6142n)), he2)
  +hx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n)), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), NA.add_comm(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n), 2180n), N.sub_add(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n, he))
  +hXl = Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(XY, 200n), 1n), Nat.add(3971n, 201n)), Nat.is_le(Nat.add(XY, 201n), Nat.add(3971n, 201n)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(3971n, 201n)), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(XY, 200n), Nat.add(XY, 200n), Equal.trans(Nat, Nat.add(XY, 200n), Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, 200n), Equal.cong(Nat, Nat, z => Nat.add(z, 200n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, Nat.add(0n, 200n)), Nat.add(XY, 200n), NA.add_assoc(XY, 0n, 200n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, Nat.add(200n, 1n)), Nat.add(XY, 201n), NA.add_assoc(XY, 200n, 1n), {==})), Equal.sym(Nat, Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==}))))), Equal.trans(Bool, Nat.is_le(Nat.add(XY, 201n), Nat.add(3971n, 201n)), Nat.is_le(XY, 3971n), True{}, FR.le_cancel_r(XY, 3971n, 201n), hXY))
  +hXx = Equal.trans(Bool, Nat.is_le(Nat.add(1926n, 3000n), Nat.add(XX, 3000n)), Nat.is_le(1926n, XX), True{}, FR.le_cancel_r(1926n, XX, 3000n), hXX)
  +hXle = N.le_trans(Nat.add(Nat.add(XY, 200n), 1n), 4926n, Nat.add(XX, 3000n), N.le_trans(Nat.add(Nat.add(XY, 200n), 1n), 4172n, 4926n, hXl, {==}), hXx)
  +ha = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(XY, 201n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), N.add_zero(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), z), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.add(XY, 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(0n, Nat.add(XY, 201n))), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), NA.add_assoc(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n, Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), z), Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_swap(0n, XY, 201n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(XY, 200n), 1n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(XY, 200n), Nat.add(XY, 200n), Equal.trans(Nat, Nat.add(XY, 200n), Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, 200n), Equal.cong(Nat, Nat, z => Nat.add(z, 200n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 200n), Nat.add(XY, Nat.add(0n, 200n)), Nat.add(XY, 200n), NA.add_assoc(XY, 0n, 200n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(XY, 200n), 1n), Nat.add(XY, Nat.add(200n, 1n)), Nat.add(XY, 201n), NA.add_assoc(XY, 200n, 1n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XY, 201n), z), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), N.add_zero(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)))))), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(XY, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(XY, Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n))), Nat.add(XY, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n)), NA.add_assoc(XY, 201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Equal.cong(Nat, Nat, z => Nat.add(XY, z), Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n), Equal.trans(Nat, Nat.add(201n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), Nat.add(201n, 0n)), Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n), NA.add_swap(201n, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 0n), {==}))), NA.add_swap(XY, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 201n))))), N.sub_add(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n), hXle))
  +hG = DX.dexp(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), XX, XY, Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)), Nat.sub(Nat.add(62n, sx), sy), sx, 1022n, sx, sy, EA, EB, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), ha, hdp, hP, hf, hEAx, hEBy, hd)
  +hEx = NR.add_cancel(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy))), Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n), Equal.trans(Nat, Nat.add(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)))), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n)), Equal.trans(Nat, Nat.add(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)))), Nat.add(Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy))), 2180n), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), NA.add_comm(2180n, Nat.add(Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), 1n+Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)))), hG), Equal.sym(Nat, Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n)), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), Equal.trans(Nat, Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n)), Nat.add(Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n), 2180n), Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), NA.add_comm(2180n, Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n)), hx))))
  DF.dgen(one, h1, s, Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), Nat.sub(Nat.sub(Nat.add(EA, Nat.add(F.off(), 1022n)), EB), 2180n), hx, A, B, Nat.sub(SW.value(B), 1n), hBp, MX, yp, sx, sy, Nat.sub(Nat.add(62n, sx), sy), Nat.sub(200n, Nat.sub(Nat.add(62n, sx), sy)), hva, hB, hP, hdp, hle, hRlt, hhi, Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n)), hEx)

def dcore_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +EA: Nat, +A: WU.U64, +EB: Nat, +B: WU.U64, +MX: Nat, +yp: Nat, +sx: Nat, +sy: Nat, +XX: Nat, +XY: Nat, +hA: {SW.value(A) == C.shift(sx, MX) : Nat}, +hB: {SW.value(B) == C.shift(sy, 1n+yp) : Nat}, +a53: {C.fits(53n, SW.value(A)) == True{} : Bool}, +a52: {C.fits(52n, SW.value(A)) == False{} : Bool}, +b53: {C.fits(53n, SW.value(B)) == True{} : Bool}, +b52: {C.fits(52n, SW.value(B)) == False{} : Bool}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hsx: {Nat.is_le(sx, 53n) == True{} : Bool}, +hsy: {Nat.is_le(sy, 53n) == True{} : Bool}, +hXX: {Nat.is_le(1926n, XX) == True{} : Bool}, +hXY: {Nat.is_le(XY, 3971n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(SW.value(A), SW.value(B)) == c : Bool}) -> {F.div_ab(s, EA, A, EB, B, c) == SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : F.F64}:
  match c:
    case True{}:
      dq_lt(one, h1, s, EA, A, EB, B, MX, yp, sx, sy, XX, XY, hA, hB, a53, a52, b53, b52, hEAx, hEBy, hsx, hsy, hXX, hXY, hc)
    case False{}:
      dq_ge(one, h1, s, EA, A, EB, B, MX, yp, sx, sy, XX, XY, hA, hB, a53, a52, b53, b52, hEAx, hEBy, hsx, hsy, hXX, hXY, hc)

def dcore(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +EA: Nat, +A: WU.U64, +EB: Nat, +B: WU.U64, +MX: Nat, +yp: Nat, +sx: Nat, +sy: Nat, +XX: Nat, +XY: Nat, +hA: {SW.value(A) == C.shift(sx, MX) : Nat}, +hB: {SW.value(B) == C.shift(sy, 1n+yp) : Nat}, +a53: {C.fits(53n, SW.value(A)) == True{} : Bool}, +a52: {C.fits(52n, SW.value(A)) == False{} : Bool}, +b53: {C.fits(53n, SW.value(B)) == True{} : Bool}, +b52: {C.fits(52n, SW.value(B)) == False{} : Bool}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hsx: {Nat.is_le(sx, 53n) == True{} : Bool}, +hsy: {Nat.is_le(sy, 53n) == True{} : Bool}, +hXX: {Nat.is_le(1926n, XX) == True{} : Bool}, +hXY: {Nat.is_le(XY, 3971n) == True{} : Bool}) -> {F.div_n(s, EA, A, EB, B) == SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : F.F64}:
  lt = WA.lt_value(A, B)
  +e1 = Equal.cong(Bool, F.F64, t => F.div_ab(s, EA, A, EB, B, t), X.lt(A, B), Nat.is_lt(SW.value(A), SW.value(B)), lt)
  Equal.trans(F.F64, F.div_n(s, EA, A, EB, B), F.div_ab(s, EA, A, EB, B, Nat.is_lt(SW.value(A), SW.value(B))), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))), e1, dcore_c(one, h1, s, EA, A, EB, B, MX, yp, sx, sy, XX, XY, hA, hB, a53, a52, b53, b52, hEAx, hEBy, hsx, hsy, hXX, hXY, Nat.is_lt(SW.value(A), SW.value(B)), {==}))