import Base
import ./f64light.bend as FL
import ../../../spec/lib/common.bend as C
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 ./f64rtools.bend as RT
import ./natfuel.bend as NF

# The quotient and sticky bit of a division, at two scales: the spec's
# 2 * floor(MX * 2^200 / MY) + [remainder != 0] cut at bit d is floor(MX *
# 2^P / MY) with the same sticky bit (P + d = 201), and SoftFloat's two
# 32-bit digits of (a - b) * 2^64 / b give floor(a * 2^62 / b) and its
# sticky bit.

def add_eq0(+a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
  FL.add_eq0(a, b)

def mul_eq0(+a: Nat, +yp: Nat) -> {Nat.is_eq(Nat.mul(a, 1n+yp), 0n) == Nat.is_eq(a, 0n) : Bool}:
  match a:
    case 0n:
      {==}
    case 1n+ +ap:
      {==}

def min1_eq0(+b: Nat) -> {Nat.is_eq(Nat.min(b, 1n), 0n) == Nat.is_eq(b, 0n) : Bool}:
  match b:
    case 0n:
      {==}
    case 1n+ +bq:
      {==}

def min1_le(+b: Nat) -> {Nat.is_le(Nat.min(b, 1n), 1n) == True{} : Bool}:
  match b:
    case 0n:
      {==}
    case 1n+ +bq:
      match bq:
        case 0n:
          {==}
        case 1n+ +bz:
          {==}

def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
  match a b:
    case True{} True{}:
      {==}
    case True{} False{}:
      {==}
    case False{} True{}:
      {==}
    case False{} False{}:
      {==}

def mul1(+y: Nat) -> {Nat.mul(1n, y) == y : Nat}:
  Equal.trans(Nat, Nat.mul(1n, y), Nat.mul(y, 1n), y, NA.mul_comm(1n, y), NA.mul_one(y))

# 2^k * y as a product
def sh_y(+k: Nat, +y: Nat) -> {Nat.mul(C.shift(k, 1n), y) == C.shift(k, y) : Nat}:
  Equal.trans(Nat, Nat.mul(C.shift(k, 1n), y), C.shift(k, Nat.mul(1n, y)), C.shift(k, y), WW.shift_mul_l(k, 1n, y), Equal.cong(Nat, Nat, z => C.shift(k, z), Nat.mul(1n, y), y, mul1(y)))

# le/lt under a common shift
def le_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_le(C.shift(k, a), C.shift(k, b)) == Nat.is_le(a, b) : Bool}:
  Equal.cong(Cmp, Bool, c => Cmp.is_le(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))

def lt_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == Nat.is_lt(a, b) : Bool}:
  Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))

# the spec's significand cut at bit 1+dp, where P + dp = 200
def specA(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat, +hP: {Nat.add(dp, P) == 200n : Nat}) -> {Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))) == 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}:
  +e0 = NR.dm_eq(yp, C.shift(P, MX))
  +e1 = Equal.trans(Nat, C.shift(200n, MX), C.shift(Nat.add(dp, P), MX), C.shift(dp, C.shift(P, MX)), Equal.cong(Nat, Nat, z => C.shift(z, MX), 200n, Nat.add(dp, P), Equal.sym(Nat, Nat.add(dp, P), 200n, hP)), WW.shift_comp(dp, P, MX))
  +e2 = Equal.cong(Nat, Nat, z => C.shift(dp, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), e0)
  +e3 = WW.shift_add(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))
  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_l(dp, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))
  +e5 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), z), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))))
  +e6 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_assoc(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
  +e7 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), NA.mul_add_right(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)))
  +eN = Equal.trans(Nat, C.shift(200n, MX), C.shift(dp, C.shift(P, MX)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e1, Equal.trans(Nat, C.shift(dp, C.shift(P, MX)), C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e2, Equal.trans(Nat, C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e3, Equal.trans(Nat, Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e4, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e5, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e6, e7))))))
  +hb = NR.dm_lt(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))
  +eD = Equal.trans(Nat, Nat.div(C.shift(200n, MX), 1n+yp), Nat.div(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.div_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))
  +eR = Equal.trans(Nat, Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.mod_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))
  +m1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, z), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.div(C.shift(200n, MX), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eD)
  +m2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(z, 1n)), Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), eR)
  +m3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Equal.sym(Nat, Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))))
  +m4 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
  +m5 = NA.add_assoc(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))
  +m6 = NA.add_comm(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))
  +m7 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_comm(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))
  +ch = Equal.trans(Nat, 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.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m1, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m2, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m3, Equal.trans(Nat, Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m4, Equal.trans(Nat, Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m5, Equal.trans(Nat, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m6, m7))))))
  Equal.sym(Nat, 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.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), ch)

# the low part fits 1+dp bits
def specA_fit(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {C.fits(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))) == True{} : Bool}:
  +l1 = Equal.trans(Bool, Nat.is_le(C.shift(dp, 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.is_le(Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), False{}, NR.le_div(yp, C.shift(dp, 1n), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Equal.trans(Bool, Nat.is_le(Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.is_le(C.shift(dp, 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, 1n+yp), sh_y(dp, 1n+yp)), Equal.trans(Bool, Nat.is_le(C.shift(dp, 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.is_le(1n+yp, Nat.mod(C.shift(P, MX), 1n+yp)), False{}, le_sh(dp, 1n+yp, Nat.mod(C.shift(P, MX), 1n+yp)), N.lt_not_le(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp, NR.dm_lt(yp, C.shift(P, MX))))))
  +l2 = N.not_le_lt(C.shift(dp, 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), l1)
  +fa = WW.fits_one(dp, 1n, {==}, Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), l2)
  Equal.trans(Bool, C.fits(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), C.fits(dp, Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), True{}, RT.fit_td(dp, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), min1_le(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), fa)

# the low part is zero exactly when MX * 2^P is a multiple of MY
def specA_z(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:
  +z1 = add_eq0(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
  +z2 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), min1_eq0(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
  +z3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), t), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), WW.dbl_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
  +z4 = and_comm(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n))
  +z5 = Equal.sym(Bool, Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), mul_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), yp))
  +z6 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), z5)
  +z7 = Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), add_eq0(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
  +z8 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))))
  +z9 = WW.shift_eq0(dp, Nat.mod(C.shift(P, MX), 1n+yp))
  Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n), Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z1, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z2, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z3, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z4, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z6, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z7, Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z8, z9)))))))


# SoftFloat's quotient: (a - b) * 2^64 = Q * b + r2 with r2 < b gives
# a * 2^62 = T * b + e with T = 2^62 + floor(Q / 4) and e < b
def iq_parts(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)) == C.shift(2n, C.shift(62n, R)) : Nat}:
  +q1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, B), r2), Q, Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), WW.low_high(2n, Q))
  +q2 = Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), NA.mul_add_right(C.low(2n, Q), C.shift(2n, C.high(2n, Q)), B))
  +q3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), z), r2), Nat.mul(C.shift(2n, C.high(2n, Q)), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), WW.shift_mul_l(2n, C.high(2n, Q), B))
  +q4 = NA.add_assoc(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)
  +q5 = NA.add_swap(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)
  +q7 = Equal.trans(Nat, C.shift(64n, R), C.shift(Nat.add(2n, 62n), R), C.shift(2n, C.shift(62n, R)), {==}, WW.shift_comp(2n, 62n, R))
  +x1 = Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q1, Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q2, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q3, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q4, q5))))
  Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), Nat.add(Nat.mul(Q, B), r2), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), x1), Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), C.shift(64n, R), C.shift(2n, C.shift(62n, R)), hQ, q7))

# h * b <= (a - b) * 2^62
def iq_le(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)) == True{} : Bool}:
  +p = iq_parts(B, R, Q, r2, hQ)
  +l = L.subst(Nat, z => {Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), z) == True{} : Bool}, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p, N.le_add_right(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)))
  Equal.trans(Bool, Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), True{}, Equal.sym(Bool, Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), le_sh(2n, Nat.mul(C.high(2n, Q), B), C.shift(62n, R))), l)

# the remainder e = (a - b) * 2^62 - h * b, and 4 e = low2(Q) * b + r2
def iq_eps(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))) == Nat.add(Nat.mul(C.low(2n, Q), B), r2) : Nat}:
  +p = iq_parts(B, R, Q, r2, hQ)
  +e1 = N.sub_add(C.shift(62n, R), Nat.mul(C.high(2n, Q), B), iq_le(B, R, Q, r2, hQ))
  +e2 = Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), WW.shift_add(2n, Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Equal.cong(Nat, Nat, z => C.shift(2n, z), Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), C.shift(62n, R), e1))
  NR.add_cancel(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), Nat.add(Nat.mul(C.low(2n, Q), B), r2), Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), e2, Equal.sym(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p)))

def low2_le(+Q: Nat, +bp: Nat) -> {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), C.shift(2n, 1n+bp)) == True{} : Bool}:
  +l = N.lt_succ_le_succ(C.low(2n, Q), 4n, WW.low_lt(2n, Q))
  +m = NF.mul_le_r(1n+bp, 1n+C.low(2n, Q), 4n, l)
  +e = Equal.trans(Nat, Nat.mul(1n+bp, 4n), Nat.mul(4n, 1n+bp), C.shift(2n, 1n+bp), NA.mul_comm(1n+bp, 4n), sh_y(2n, 1n+bp))
  L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), z) == True{} : Bool}, Nat.mul(1n+bp, 4n), C.shift(2n, 1n+bp), e, L.subst(Nat, z => {Nat.is_le(z, Nat.mul(1n+bp, 4n)) == True{} : Bool}, Nat.mul(1n+bp, 1n+C.low(2n, Q)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.mul_comm(1n+bp, 1n+C.low(2n, Q)), m))

# e < b
def iq_lt(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}, +hr2: {Nat.is_lt(r2, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp) == True{} : Bool}:
  +E = Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2)
  +l1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp)), Nat.is_lt(r2, 1n+bp), True{}, WW.lt_cancel_l(Nat.mul(C.low(2n, Q), 1n+bp), r2, 1n+bp), hr2)
  +e1 = Equal.trans(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.add(1n+bp, Nat.mul(C.low(2n, Q), 1n+bp)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.add_comm(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), {==})
  +l2 = N.lt_le_trans(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), C.shift(2n, 1n+bp), l1, L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.mul(1n+C.low(2n, Q), 1n+bp), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Equal.sym(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.mul(1n+C.low(2n, Q), 1n+bp), e1), low2_le(Q, bp)))
  +l3 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Equal.sym(Nat, C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ)), l2)
  Equal.trans(Bool, Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), True{}, Equal.sym(Bool, Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), lt_sh(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp)), l3)

# e is zero exactly when the low two quotient bits and r2 are
def iq_z(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n) == Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)) : Bool}:
  +z1 = Equal.sym(Bool, Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n), WW.shift_eq0(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))))
  +z2 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ))
  +z3 = add_eq0(Nat.mul(C.low(2n, Q), 1n+bp), r2)
  +z4 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(r2, 0n)), Nat.is_eq(Nat.mul(C.low(2n, Q), 1n+bp), 0n), Nat.is_eq(C.low(2n, Q), 0n), mul_eq0(C.low(2n, Q), bp))
  Equal.trans(Bool, Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n), Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z1, Equal.trans(Bool, Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Nat.is_eq(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), 0n), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z2, Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), 0n), Bool.and(Nat.is_eq(Nat.mul(C.low(2n, Q), 1n+bp), 0n), Nat.is_eq(r2, 0n)), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z3, z4)))


# the two scales agree: a * 2^62 = T * b + e with e < b, a = MX * 2^u and
# b = MY * 2^w give T = floor(MX * 2^P / MY) and e = 0 iff MY | MX * 2^P
def jn_eq(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {C.shift(62n, C.shift(u, MX)) == Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))) : Nat}:
  +j1 = Equal.sym(Nat, C.shift(Nat.add(62n, u), MX), C.shift(62n, C.shift(u, MX)), WW.shift_comp(62n, u, MX))
  +j2 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(62n, u), Nat.add(w, P), hP)
  +j3 = WW.shift_comp(w, P, MX)
  +j4 = Equal.cong(Nat, Nat, z => C.shift(w, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), NR.dm_eq(yp, C.shift(P, MX)))
  +j5 = WW.shift_add(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))
  +j6 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), Equal.sym(Nat, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_r(w, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))
  +j7 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), z), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(w, 1n+yp), 1n+bp, hB)
  Equal.trans(Nat, C.shift(62n, C.shift(u, MX)), C.shift(Nat.add(62n, u), MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j1, Equal.trans(Nat, C.shift(Nat.add(62n, u), MX), C.shift(Nat.add(w, P), MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j2, Equal.trans(Nat, C.shift(Nat.add(w, P), MX), C.shift(w, C.shift(P, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j3, Equal.trans(Nat, C.shift(w, C.shift(P, MX)), C.shift(w, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j4, Equal.trans(Nat, C.shift(w, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j5, Equal.trans(Nat, Nat.add(C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j6, j7))))))

def jn_lt(+MX: Nat, +yp: Nat, +w: Nat, +P: Nat, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+bp) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), z) == True{} : Bool}, C.shift(w, 1n+yp), 1n+bp, hB, Equal.trans(Bool, Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), C.shift(w, 1n+yp)), Nat.is_lt(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), True{}, lt_sh(w, Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), NR.dm_lt(yp, C.shift(P, MX))))

def jn_q(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {T == Nat.div(C.shift(P, MX), 1n+yp) : Nat}:
  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))
  +dT = NR.div_of(T, bp, e, he)
  +dQ = NR.div_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))
  Equal.trans(Nat, T, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.div(C.shift(P, MX), 1n+yp), Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), T, dT), Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.div(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), Nat.div(C.shift(P, MX), 1n+yp), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), dQ))

def jn_z(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {Nat.is_eq(e, 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:
  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))
  +mT = NR.mod_of(T, bp, e, he)
  +mQ = NR.mod_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))
  +ee = Equal.trans(Nat, e, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), e, mT), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.mod(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), mQ))
  Equal.trans(Bool, Nat.is_eq(e, 0n), Nat.is_eq(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), e, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), ee), WW.shift_eq0(w, Nat.mod(C.shift(P, MX), 1n+yp)))