import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./natlight.bend as QN

# Montgomery reduction on naturals (Montgomery, "Modular multiplication
# without trial division", 1985): with R = 2^64 and m mp = -1 mod R,
# u = (t mp mod R) makes t + u m divisible by R; and for odd m, x R = y R
# (mod m) gives x = y (mod m), by the inverse (m + 1) / 2 of 2.

def low_addlow(+kk: Nat, +a: Nat, +b: Nat) -> {C.low(kk, Nat.add(a, C.low(kk, b))) == C.low(kk, Nat.add(a, b)) : Nat}:
  Equal.sym(Nat, C.low(kk, Nat.add(a, b)), C.low(kk, Nat.add(a, C.low(kk, b))), Equal.trans(Nat, C.low(kk, Nat.add(a, b)), C.low(kk, Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b))))), C.low(kk, Nat.add(a, C.low(kk, b))), Equal.cong(Nat, Nat, z => C.low(kk, Nat.add(a, z)), b, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b))), WW.low_high(kk, b)), Equal.trans(Nat, C.low(kk, Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b))))), C.low(kk, Nat.add(Nat.add(a, C.low(kk, b)), C.shift(kk, C.high(kk, b)))), C.low(kk, Nat.add(a, C.low(kk, b))), Equal.cong(Nat, Nat, z => C.low(kk, z), Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b)))), Nat.add(Nat.add(a, C.low(kk, b)), C.shift(kk, C.high(kk, b))), Equal.sym(Nat, Nat.add(Nat.add(a, C.low(kk, b)), C.shift(kk, C.high(kk, b))), Nat.add(a, Nat.add(C.low(kk, b), C.shift(kk, C.high(kk, b)))), NA.add_assoc(a, C.low(kk, b), C.shift(kk, C.high(kk, b))))), WW.low_add_shift(kk, Nat.add(a, C.low(kk, b)), C.high(kk, b)))))

def low_mullow(+kk: Nat, +a: Nat, +b: Nat) -> {C.low(kk, Nat.mul(C.low(kk, a), b)) == C.low(kk, Nat.mul(a, b)) : Nat}:
  Equal.sym(Nat, C.low(kk, Nat.mul(a, b)), C.low(kk, Nat.mul(C.low(kk, a), b)), Equal.trans(Nat, C.low(kk, Nat.mul(a, b)), C.low(kk, Nat.mul(Nat.add(C.low(kk, a), C.shift(kk, C.high(kk, a))), b)), C.low(kk, Nat.mul(C.low(kk, a), b)), Equal.cong(Nat, Nat, z => C.low(kk, Nat.mul(z, b)), a, Nat.add(C.low(kk, a), C.shift(kk, C.high(kk, a))), WW.low_high(kk, a)), Equal.trans(Nat, C.low(kk, Nat.mul(Nat.add(C.low(kk, a), C.shift(kk, C.high(kk, a))), b)), C.low(kk, Nat.add(Nat.mul(C.low(kk, a), b), Nat.mul(C.shift(kk, C.high(kk, a)), b))), C.low(kk, Nat.mul(C.low(kk, a), b)), Equal.cong(Nat, Nat, z => C.low(kk, z), Nat.mul(Nat.add(C.low(kk, a), C.shift(kk, C.high(kk, a))), b), Nat.add(Nat.mul(C.low(kk, a), b), Nat.mul(C.shift(kk, C.high(kk, a)), b)), NA.mul_add_right(C.low(kk, a), C.shift(kk, C.high(kk, a)), b)), Equal.trans(Nat, C.low(kk, Nat.add(Nat.mul(C.low(kk, a), b), Nat.mul(C.shift(kk, C.high(kk, a)), b))), C.low(kk, Nat.add(Nat.mul(C.low(kk, a), b), C.shift(kk, Nat.mul(C.high(kk, a), b)))), C.low(kk, Nat.mul(C.low(kk, a), b)), Equal.cong(Nat, Nat, z => C.low(kk, Nat.add(Nat.mul(C.low(kk, a), b), z)), Nat.mul(C.shift(kk, C.high(kk, a)), b), C.shift(kk, Nat.mul(C.high(kk, a), b)), WW.shift_mul_l(kk, C.high(kk, a), b)), WW.low_add_shift(kk, Nat.mul(C.low(kk, a), b), Nat.mul(C.high(kk, a), b))))))

def low_zero(k: Nat) -> {C.low(k, 0n) == 0n : Nat}:
  match k:
    case 0n:
      {==}
    case 1n+ +p:
      Equal.cong(Nat, Nat, z => Nat.double(z), C.low(p, 0n), 0n, low_zero(p))

def low_shift0(+kk: Nat, +z: Nat) -> {C.low(kk, C.shift(kk, z)) == 0n : Nat}:
  Equal.trans(Nat, C.low(kk, C.shift(kk, z)), C.low(kk, 0n), 0n, WW.low_add_shift(kk, 0n, z), low_zero(kk))

# t + (t mp mod R) m == 0 (mod R) for m mp == -1 (mod R)
def redc0(+kk: Nat, +one: Nat, +tl: Nat, +M: Nat, +mp: Nat, +hinv: {1n+C.low(kk, Nat.mul(M, mp)) == C.shift(kk, one) : Nat}) -> {C.low(kk, Nat.add(tl, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M))) == 0n : Nat}:
  Equal.trans(Nat, C.low(kk, Nat.add(tl, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M))), C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M)))), 0n, Equal.sym(Nat, C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M)))), C.low(kk, Nat.add(tl, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M))), low_addlow(kk, tl, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M))), Equal.trans(Nat, C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M)))), C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(Nat.mul(tl, mp), M)))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, Nat.add(tl, z)), C.low(kk, Nat.mul(C.low(kk, Nat.mul(tl, mp)), M)), C.low(kk, Nat.mul(Nat.mul(tl, mp), M)), low_mullow(kk, Nat.mul(tl, mp), M)), Equal.trans(Nat, C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(Nat.mul(tl, mp), M)))), C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(tl, Nat.mul(mp, M))))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, Nat.add(tl, C.low(kk, z))), Nat.mul(Nat.mul(tl, mp), M), Nat.mul(tl, Nat.mul(mp, M)), NA.mul_assoc(tl, mp, M)), Equal.trans(Nat, C.low(kk, Nat.add(tl, C.low(kk, Nat.mul(tl, Nat.mul(mp, M))))), C.low(kk, Nat.add(tl, Nat.mul(tl, Nat.mul(mp, M)))), 0n, low_addlow(kk, tl, Nat.mul(tl, Nat.mul(mp, M))), Equal.trans(Nat, C.low(kk, Nat.add(tl, Nat.mul(tl, Nat.mul(mp, M)))), C.low(kk, Nat.mul(tl, 1n+Nat.mul(mp, M))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, z), Nat.add(tl, Nat.mul(tl, Nat.mul(mp, M))), Nat.mul(tl, 1n+Nat.mul(mp, M)), Equal.sym(Nat, Nat.mul(tl, 1n+Nat.mul(mp, M)), Nat.add(tl, Nat.mul(tl, Nat.mul(mp, M))), NA.mul_succ(tl, Nat.mul(mp, M)))), Equal.trans(Nat, C.low(kk, Nat.mul(tl, 1n+Nat.mul(mp, M))), C.low(kk, Nat.mul(tl, 1n+Nat.add(C.low(kk, Nat.mul(M, mp)), C.shift(kk, C.high(kk, Nat.mul(M, mp)))))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, Nat.mul(tl, 1n+z)), Nat.mul(mp, M), Nat.add(C.low(kk, Nat.mul(M, mp)), C.shift(kk, C.high(kk, Nat.mul(M, mp)))), Equal.trans(Nat, Nat.mul(mp, M), Nat.mul(M, mp), Nat.add(C.low(kk, Nat.mul(M, mp)), C.shift(kk, C.high(kk, Nat.mul(M, mp)))), NA.mul_comm(mp, M), WW.low_high(kk, Nat.mul(M, mp)))), Equal.trans(Nat, C.low(kk, Nat.mul(tl, 1n+Nat.add(C.low(kk, Nat.mul(M, mp)), C.shift(kk, C.high(kk, Nat.mul(M, mp)))))), C.low(kk, Nat.mul(tl, Nat.add(C.shift(kk, one), C.shift(kk, C.high(kk, Nat.mul(M, mp)))))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, Nat.mul(tl, Nat.add(z, C.shift(kk, C.high(kk, Nat.mul(M, mp)))))), 1n+C.low(kk, Nat.mul(M, mp)), C.shift(kk, one), hinv), Equal.trans(Nat, C.low(kk, Nat.mul(tl, Nat.add(C.shift(kk, one), C.shift(kk, C.high(kk, Nat.mul(M, mp)))))), C.low(kk, Nat.mul(tl, C.shift(kk, Nat.add(one, C.high(kk, Nat.mul(M, mp)))))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, Nat.mul(tl, z)), Nat.add(C.shift(kk, one), C.shift(kk, C.high(kk, Nat.mul(M, mp)))), C.shift(kk, Nat.add(one, C.high(kk, Nat.mul(M, mp)))), Equal.sym(Nat, C.shift(kk, Nat.add(one, C.high(kk, Nat.mul(M, mp)))), Nat.add(C.shift(kk, one), C.shift(kk, C.high(kk, Nat.mul(M, mp)))), WW.shift_add(kk, one, C.high(kk, Nat.mul(M, mp))))), Equal.trans(Nat, C.low(kk, Nat.mul(tl, C.shift(kk, Nat.add(one, C.high(kk, Nat.mul(M, mp)))))), C.low(kk, C.shift(kk, Nat.mul(tl, Nat.add(one, C.high(kk, Nat.mul(M, mp)))))), 0n, Equal.cong(Nat, Nat, z => C.low(kk, z), Nat.mul(tl, C.shift(kk, Nat.add(one, C.high(kk, Nat.mul(M, mp))))), C.shift(kk, Nat.mul(tl, Nat.add(one, C.high(kk, Nat.mul(M, mp))))), WW.shift_mul_r(kk, tl, Nat.add(one, C.high(kk, Nat.mul(M, mp))))), low_shift0(kk, Nat.mul(tl, Nat.add(one, C.high(kk, Nat.mul(M, mp))))))))))))))

# x == 2 x (m + 1) / 2 (mod m)
def half_inv(+bp: Nat, +hh: Nat, +hM: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +x: Nat) -> {Nat.mod(x, 1n+bp) == Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp) : Nat}:
  Equal.trans(Nat, Nat.mod(x, 1n+bp), Nat.mod(Nat.add(Nat.mul(x, 1n+bp), x), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(x, 1n+bp), x), 1n+bp), Nat.mod(x, 1n+bp), NR.absorb(bp, x, x)), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(x, 1n+bp), x), 1n+bp), Nat.mod(Nat.mul(x, 1n+1n+bp), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(x, 1n+bp), x), Nat.mul(x, 1n+1n+bp), Equal.trans(Nat, Nat.add(Nat.mul(x, 1n+bp), x), Nat.add(x, Nat.mul(x, 1n+bp)), Nat.mul(x, 1n+1n+bp), NA.add_comm(Nat.mul(x, 1n+bp), x), Equal.sym(Nat, Nat.mul(x, 1n+1n+bp), Nat.add(x, Nat.mul(x, 1n+bp)), NA.mul_succ(x, 1n+bp)))), Equal.trans(Nat, Nat.mod(Nat.mul(x, 1n+1n+bp), 1n+bp), Nat.mod(Nat.mul(x, Nat.add(hh, hh)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(x, z), 1n+bp), 1n+1n+bp, Nat.add(hh, hh), hM), Equal.trans(Nat, Nat.mod(Nat.mul(x, Nat.add(hh, hh)), 1n+bp), Nat.mod(Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(x, Nat.add(hh, hh)), Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), NA.mul_add_left(x, hh, hh)), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), 1n+bp), Nat.mod(Nat.mul(Nat.add(x, x), hh), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), Nat.mul(Nat.add(x, x), hh), Equal.sym(Nat, Nat.mul(Nat.add(x, x), hh), Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), NA.mul_add_right(x, x, hh))), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.add(x, x), hh), 1n+bp), Nat.mod(Nat.mul(Nat.double(x), hh), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(z, hh), 1n+bp), Nat.add(x, x), Nat.double(x), Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x))), Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Nat.mod(Nat.mul(Nat.double(x), hh), 1n+bp), NR.mod_mul_l(bp, Nat.double(x), hh))))))))

# 2 x == 2 y (mod m) gives x == y (mod m) for odd m
def cancel2(+bp: Nat, +hh: Nat, +hM: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +x: Nat, +y: Nat, +h: {Nat.mod(Nat.double(x), 1n+bp) == Nat.mod(Nat.double(y), 1n+bp) : Nat}) -> {Nat.mod(x, 1n+bp) == Nat.mod(y, 1n+bp) : Nat}:
  Equal.trans(Nat, Nat.mod(x, 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Nat.mod(y, 1n+bp), half_inv(bp, hh, hM, x), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(y), 1n+bp), hh), 1n+bp), Nat.mod(y, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(z, hh), 1n+bp), Nat.mod(Nat.double(x), 1n+bp), Nat.mod(Nat.double(y), 1n+bp), h), Equal.sym(Nat, Nat.mod(y, 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(y), 1n+bp), hh), 1n+bp), half_inv(bp, hh, hM, y))))

# x 2^k == y 2^k (mod m) gives x == y (mod m) for odd m
def cancel(+bp: Nat, +hh: Nat, +hM: {1n+1n+bp == Nat.add(hh, hh) : Nat}, k: Nat, +x: Nat, +y: Nat, +h: {Nat.mod(C.shift(k, x), 1n+bp) == Nat.mod(C.shift(k, y), 1n+bp) : Nat}) -> {Nat.mod(x, 1n+bp) == Nat.mod(y, 1n+bp) : Nat}:
  match k:
    case 0n:
      h
    case 1n+ +j:
      cancel(bp, hh, hM, j, x, y, cancel2(bp, hh, hM, C.shift(j, x), C.shift(j, y), h))

# (z mod m) 2^k == z 2^k (mod m)
def mod_shift(+bp: Nat, +k: Nat, +z0: Nat) -> {Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp) == Nat.mod(C.shift(k, z0), 1n+bp) : Nat}:
  Equal.sym(Nat, Nat.mod(C.shift(k, z0), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.trans(Nat, Nat.mod(C.shift(k, z0), 1n+bp), Nat.mod(C.shift(k, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(k, z), 1n+bp), z0, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp)), NR.dm_eq(bp, z0)), Equal.trans(Nat, Nat.mod(C.shift(k, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(Nat.add(C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), C.shift(k, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), Nat.add(C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp))), WW.shift_add(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), Equal.trans(Nat, Nat.mod(Nat.add(C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(Nat.add(Nat.mul(C.shift(k, Nat.div(z0, 1n+bp)), 1n+bp), C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(z, C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), Nat.mul(C.shift(k, Nat.div(z0, 1n+bp)), 1n+bp), Equal.sym(Nat, Nat.mul(C.shift(k, Nat.div(z0, 1n+bp)), 1n+bp), C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), WW.shift_mul_l(k, Nat.div(z0, 1n+bp), 1n+bp))), NR.absorb(bp, C.shift(k, Nat.div(z0, 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp)))))))

def plus1(+x: Nat) -> {Nat.add(x, 1n) == 1n+x : Nat}:
  Equal.trans(Nat, Nat.add(x, 1n), 1n+Nat.add(x, 0n), 1n+x, N.add_succ(x, 0n), N.succ_cong(Nat.add(x, 0n), x, N.add_zero(x)))

# m + 1 == 2 hh for odd m, hh = m / 2 + 1
def odd_hh(+bp: Nat, +hodd: {Nat.mod(1n+bp, 2n) == 1n : Nat}) -> {1n+1n+bp == Nat.add(1n+Nat.div(1n+bp, 2n), 1n+Nat.div(1n+bp, 2n)) : Nat}:
  +e1 = Equal.trans(Nat, 1n+bp, Nat.add(Nat.mul(Nat.div(1n+bp, 2n), 2n), Nat.mod(1n+bp, 2n)), 1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), NR.dm_eq(1n, 1n+bp), Equal.trans(Nat, Nat.add(Nat.mul(Nat.div(1n+bp, 2n), 2n), Nat.mod(1n+bp, 2n)), Nat.add(Nat.mul(Nat.div(1n+bp, 2n), 2n), 1n), 1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.div(1n+bp, 2n), 2n), z), Nat.mod(1n+bp, 2n), 1n, hodd), Equal.trans(Nat, Nat.add(Nat.mul(Nat.div(1n+bp, 2n), 2n), 1n), Nat.add(Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), 1n), 1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.mul(Nat.div(1n+bp, 2n), 2n), Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), QN.two_mul(Nat.div(1n+bp, 2n))), plus1(Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n))))))
  +e2 = Equal.cong(Nat, Nat, w => 1n+w, 1n+bp, 1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), e1)
  Equal.trans(Nat, 1n+1n+bp, 1n+1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), Nat.add(1n+Nat.div(1n+bp, 2n), 1n+Nat.div(1n+bp, 2n)), e2, Equal.sym(Nat, Nat.add(1n+Nat.div(1n+bp, 2n), 1n+Nat.div(1n+bp, 2n)), 1n+1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), Equal.cong(Nat, Nat, w => 1n+w, Nat.add(Nat.div(1n+bp, 2n), 1n+Nat.div(1n+bp, 2n)), 1n+Nat.add(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)), N.add_succ(Nat.div(1n+bp, 2n), Nat.div(1n+bp, 2n)))))