# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/consts.src; edit the .src
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../lib/nat.bend as N
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./ineq.bend as I
import ./bounds.bend as B

# The constants of spec/crypto/secp256k1/field.bend, kept symbolic in one:
# 2^256 - p = 2^32 + 977 < 2^33, 2^256 - n < 2^129, and the bounds the
# folding reductions need. No 256-bit number is ever formed: every
# comparison with a closed number is of a small one (977, a 16-bit digit).

def T(+one: Nat) -> Nat:
  C.shift(256n, one)

# ---- powers of two ----

def shift_twice(+k: Nat, +x: Nat) -> {Nat.add(C.shift(k, x), C.shift(k, x)) == C.shift(1n+k, x) : Nat}:
  Equal.sym(Nat, Nat.double(C.shift(k, x)), Nat.add(C.shift(k, x), C.shift(k, x)), NA.double_self(C.shift(k, x)))

# 2^k x <= 2^(d + k) x
def shift_more(d: Nat, +k: Nat, +x: Nat) -> {Nat.is_le(C.shift(k, x), C.shift(Nat.add(d, k), x)) == True{} : Bool}:
  match d:
    case 0n:
      N.le_refl(C.shift(k, x))
    case 1n+ +e:
      N.le_trans(C.shift(k, x), C.shift(Nat.add(e, k), x), Nat.double(C.shift(Nat.add(e, k), x)), shift_more(e, k, x), N.double_self_le(C.shift(Nat.add(e, k), x)))

def shift_le_k(+j: Nat, +k: Nat, +x: Nat, +d: Nat, +hd: {Nat.add(d, j) == k : Nat}) -> {Nat.is_le(C.shift(j, x), C.shift(k, x)) == True{} : Bool}:
  I.le_subst_r(C.shift(j, x), C.shift(Nat.add(d, j), x), C.shift(k, x), Equal.cong(Nat, Nat, z => C.shift(z, x), Nat.add(d, j), k, hd), shift_more(d, j, x))

# 2^a 2^b = 2^(a + b)
def shift_mul2(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +b: Nat) -> {Nat.mul(C.shift(a, one), C.shift(b, one)) == C.shift(Nat.add(a, b), one) : Nat}:
  %Equal.sym(Nat, Nat.mul(C.shift(a, one), C.shift(b, one)), C.shift(a, Nat.mul(one, C.shift(b, one))), WW.shift_mul_l(a, one, C.shift(b, one))) : {_ == C.shift(Nat.add(a, b), one) : Nat}
  %Equal.sym(Nat, Nat.mul(one, C.shift(b, one)), C.shift(b, one), LV.mul_one_l(one, h1, C.shift(b, one))) : {C.shift(a, _) == C.shift(Nat.add(a, b), one) : Nat}
  %Equal.sym(Nat, C.shift(a, C.shift(b, one)), C.shift(Nat.add(a, b), one), SR.shift_shift(a, b, one)) : {_ == C.shift(Nat.add(a, b), one) : Nat}
  {==}

# 0 < 2^k
def shift_pos(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.is_lt(0n, C.shift(k, one)) == True{} : Bool}:
  %Equal.sym(Nat, 0n, C.shift(k, 0n), Equal.sym(Nat, C.shift(k, 0n), 0n, WW.shift_zero(k))) : {Nat.is_lt(_, C.shift(k, one)) == True{} : Bool}
  I.shift_lt(k, 0n, one, B.lt_one(one, h1))

# a small closed number below 2^k
def small_le(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +a: Nat, +h: {Nat.is_le(a, C.shift(k, 1n)) == True{} : Bool}) -> {Nat.is_le(a, C.shift(k, one)) == True{} : Bool}:
  %Equal.sym(Nat, one, 1n, h1) : {Nat.is_le(a, C.shift(k, _)) == True{} : Bool}
  h

# ---- 2^256 - p = 2^32 + 977 ----

def cp_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.cp(one) == Nat.add(C.shift(32n, one), 977n) : Nat}:
  %Equal.sym(Nat, Nat.mul(one, 977n), 977n, LV.mul_one_l(one, h1, 977n)) : {Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(977n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(977n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(977n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(one, _))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(977n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, Nat.add(0n, C.shift(16n, one)), C.shift(16n, one), SR.zero_add(C.shift(16n, one))) : {Nat.add(977n, C.shift(16n, _)) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, C.shift(16n, C.shift(16n, one)), C.shift(32n, one), SR.shift_shift(16n, 16n, one)) : {Nat.add(977n, _) == Nat.add(C.shift(32n, one), 977n) : Nat}
  %Equal.sym(Nat, Nat.add(977n, C.shift(32n, one)), Nat.add(C.shift(32n, one), 977n), NA.add_comm(977n, C.shift(32n, one))) : {_ == Nat.add(C.shift(32n, one), 977n) : Nat}
  {==}

def cp_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(FS.cp(one), C.shift(33n, one)) == True{} : Bool}:
  %Equal.sym(Nat, FS.cp(one), Nat.add(C.shift(32n, one), 977n), cp_eq(one, h1)) : {Nat.is_le(_, C.shift(33n, one)) == True{} : Bool}
  %Equal.sym(Nat, C.shift(33n, one), Nat.add(C.shift(32n, one), C.shift(32n, one)), Equal.sym(Nat, Nat.add(C.shift(32n, one), C.shift(32n, one)), C.shift(33n, one), shift_twice(32n, one))) : {Nat.is_le(Nat.add(C.shift(32n, one), 977n), _) == True{} : Bool}
  I.le_add2(C.shift(32n, one), 977n, C.shift(32n, one), C.shift(32n, one), N.le_refl(C.shift(32n, one)), small_le(one, h1, 32n, 977n, {==}))

# 2^j < 2^(1 + j), and 2^j < 2^k for j < k (k = d + 1 + j)
def shift_lt_succ(+one: Nat, +h1: {one == 1n : Nat}, +j: Nat) -> {Nat.is_lt(C.shift(j, one), C.shift(1n+j, one)) == True{} : Bool}:
  %Equal.sym(Nat, Nat.double(C.shift(j, one)), Nat.add(C.shift(j, one), C.shift(j, one)), NA.double_self(C.shift(j, one))) : {Nat.is_lt(C.shift(j, one), _) == True{} : Bool}
  I.lt_add_pos(C.shift(j, one), C.shift(j, one), shift_pos(one, h1, j))

def shift_lt_k(+one: Nat, +h1: {one == 1n : Nat}, +j: Nat, +k: Nat, +d: Nat, +hd: {Nat.add(d, 1n+j) == k : Nat}) -> {Nat.is_lt(C.shift(j, one), C.shift(k, one)) == True{} : Bool}:
  N.lt_le_trans(C.shift(j, one), C.shift(1n+j, one), C.shift(k, one), shift_lt_succ(one, h1, j), shift_le_k(1n+j, k, one, d, hd))

# the fold bounds for p: 2 c < 2^256 and (1 + c) c + c <= 2^256
def cp_cc(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.add(FS.cp(one), FS.cp(one)), C.shift(256n, one)) == True{} : Bool}:
  +c = FS.cp(one)
  +s1 = I.le_add2(c, c, C.shift(33n, one), C.shift(33n, one), cp_le(one, h1), cp_le(one, h1))
  +s2 = I.le_subst_r(Nat.add(c, c), Nat.add(C.shift(33n, one), C.shift(33n, one)), C.shift(34n, one), shift_twice(33n, one), s1)
  N.le_lt_trans(Nat.add(c, c), C.shift(34n, one), C.shift(256n, one), s2, shift_lt_k(one, h1, 34n, 256n, 221n, {==}))

def cp_succ_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(1n+FS.cp(one), C.shift(34n, one)) == True{} : Bool}:
  N.lt_succ_le_succ(FS.cp(one), C.shift(34n, one), N.le_lt_trans(FS.cp(one), C.shift(33n, one), C.shift(34n, one), cp_le(one, h1), shift_lt_succ(one, h1, 33n)))

def cp_hb(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(Nat.mul(1n+FS.cp(one), FS.cp(one)), FS.cp(one)), C.shift(256n, one)) == True{} : Bool}:
  +c = FS.cp(one)
  +s1 = I.le_mul2(1n+c, c, C.shift(34n, one), C.shift(33n, one), cp_succ_le(one, h1), cp_le(one, h1))
  +s2 = I.le_subst_r(Nat.mul(1n+c, c), Nat.mul(C.shift(34n, one), C.shift(33n, one)), C.shift(67n, one), shift_mul2(one, h1, 34n, 33n), s1)
  +s3 = I.le_add2(Nat.mul(1n+c, c), c, C.shift(67n, one), C.shift(67n, one), s2, N.le_trans(c, C.shift(33n, one), C.shift(67n, one), cp_le(one, h1), shift_le_k(33n, 67n, one, 34n, {==})))
  +s4 = I.le_subst_r(Nat.add(Nat.mul(1n+c, c), c), Nat.add(C.shift(67n, one), C.shift(67n, one)), C.shift(68n, one), shift_twice(67n, one), s3)
  N.le_trans(Nat.add(Nat.mul(1n+c, c), c), C.shift(68n, one), C.shift(256n, one), s4, shift_le_k(68n, 256n, one, 188n, {==}))

# p = 1 + pp, m + c = 2^256
def pp(+one: Nat) -> Nat:
  Nat.sub(C.shift(256n, one), Nat.add(FS.cp(one), 1n))

def cp1_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(FS.cp(one), 1n), C.shift(256n, one)) == True{} : Bool}:
  +c = FS.cp(one)
  +s1 = I.lt_succ_le(c, C.shift(256n, one), N.le_lt_trans(c, Nat.add(c, c), C.shift(256n, one), N.le_add_right(c, c), cp_cc(one, h1)))
  s1

# (c + 1) + pp = 2^256
def pp_sum(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) == C.shift(256n, one) : Nat}:
  N.sub_add(C.shift(256n, one), Nat.add(FS.cp(one), 1n), cp1_le(one, h1))

def hm_p(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(1n+pp(one), FS.cp(one)) == C.shift(256n, one) : Nat}:
  %Equal.sym(Nat, C.shift(256n, one), Nat.add(Nat.add(FS.cp(one), 1n), pp(one)), Equal.sym(Nat, Nat.add(Nat.add(FS.cp(one), 1n), pp(one)), C.shift(256n, one), pp_sum(one, h1))) : {Nat.add(1n+pp(one), FS.cp(one)) == _ : Nat}
  %Equal.sym(Nat, 1n+pp(one), Nat.add(pp(one), 1n), SR.succ_add(1n, pp(one))) : {Nat.add(_, FS.cp(one)) == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(pp(one), 1n), FS.cp(one)), Nat.add(pp(one), Nat.add(1n, FS.cp(one))), NA.add_assoc(pp(one), 1n, FS.cp(one))) : {_ == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
  %Equal.sym(Nat, Nat.add(1n, FS.cp(one)), Nat.add(FS.cp(one), 1n), NA.add_comm(1n, FS.cp(one))) : {Nat.add(pp(one), _) == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
  %Equal.sym(Nat, Nat.add(pp(one), Nat.add(FS.cp(one), 1n)), Nat.add(FS.cp(one), Nat.add(pp(one), 1n)), NA.add_swap(pp(one), FS.cp(one), 1n)) : {_ == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(FS.cp(one), 1n), pp(one)), Nat.add(FS.cp(one), Nat.add(1n, pp(one))), NA.add_assoc(FS.cp(one), 1n, pp(one))) : {Nat.add(FS.cp(one), Nat.add(pp(one), 1n)) == _ : Nat}
  %Equal.sym(Nat, Nat.add(1n, pp(one)), Nat.add(pp(one), 1n), NA.add_comm(1n, pp(one))) : {Nat.add(FS.cp(one), Nat.add(pp(one), 1n)) == Nat.add(FS.cp(one), _) : Nat}
  {==}

def prime_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.prime(one) == 1n+pp(one) : Nat}:
  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+pp(one), FS.cp(one)), Equal.sym(Nat, Nat.add(1n+pp(one), FS.cp(one)), C.shift(256n, one), hm_p(one, h1))) : {Nat.sub(_, FS.cp(one)) == 1n+pp(one) : Nat}
  %Equal.sym(Nat, Nat.add(1n+pp(one), FS.cp(one)), Nat.add(FS.cp(one), 1n+pp(one)), NA.add_comm(1n+pp(one), FS.cp(one))) : {Nat.sub(_, FS.cp(one)) == 1n+pp(one) : Nat}
  N.add_sub_cancel(FS.cp(one), 1n+pp(one))

# ---- 2^256 - n < 2^129 ----

def digits_split(+one: Nat, n: Nat, ds: List<&2, Nat>) -> {FS.digits(one, ds) == Nat.add(FS.digits(one, L.take(n, ds)), LV.pos(n, FS.digits(one, L.drop(n, ds)))) : Nat}:
  match n ds:
    case 0n Nil{}:
      {==}
    case 0n d <> t:
      {==}
    case 1n+ +k Nil{}:
      %Equal.sym(Nat, LV.pos(k, 0n), 0n, LV.pos_zero(k)) : {0n == Nat.add(0n, C.shift(16n, _)) : Nat}
      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {0n == Nat.add(0n, _) : Nat}
      %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {0n == _ : Nat}
      {==}
    case 1n+ +k +d <> +t:
      %Equal.sym(Nat, FS.digits(one, t), Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t)))), digits_split(one, k, t)) : {Nat.add(Nat.mul(one, d), C.shift(16n, _)) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, Nat.mul(one, d), Nat.mul(d, one), NA.mul_comm(one, d)) : {Nat.add(_, C.shift(16n, Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t)))))) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, C.shift(16n, Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), WW.shift_add(16n, FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t))))) : {Nat.add(Nat.mul(d, one), _) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), NA.add_swap(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {_ == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), _) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, Nat.mul(one, d), Nat.mul(d, one), NA.mul_comm(one, d)) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(Nat.add(_, C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t)))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(_, C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one)), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), NA.add_assoc(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == _ : Nat}
      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), _) : Nat}
      {==}

def digits_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +ys: List<&2, Nat>, +h: {FS.limbs16(one, k, ys) == True{} : Bool}) -> {Nat.is_lt(FS.digits(one, ys), LV.pos(k, one)) == True{} : Bool}:
  %Equal.sym(Nat, FS.digits(one, ys), LV.ev(ys), LV.ev_value(one, h1, ys)) : {Nat.is_lt(_, LV.pos(k, one)) == True{} : Bool}
  B.limbs_lt(one, h1, k, ys, h)

def cn8() -> List<&2, Nat>:
  [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n]

def cn8_limbs(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 8n, cn8()) == True{} : Bool}:
  %Equal.sym(Nat, one, 1n, h1) : {FS.limbs16(_, 8n, cn8()) == True{} : Bool}
  {==}

def cn_split(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.cn(one) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}:
  %Equal.sym(Nat, FS.cn(one), Nat.add(FS.digits(one, cn8()), LV.pos(8n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))), digits_split(one, 8n, [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])) : {_ == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(FS.digits(one, cn8()), LV.pos(8n, Nat.add(_, C.shift(16n, 0n)))) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(FS.digits(one, cn8()), LV.pos(8n, Nat.add(one, _))) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(FS.digits(one, cn8()), LV.pos(8n, _)) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
  {==}

def cn_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(FS.cn(one), C.shift(129n, one)) == True{} : Bool}:
  %Equal.sym(Nat, FS.cn(one), Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)), cn_split(one, h1)) : {Nat.is_lt(_, C.shift(129n, one)) == True{} : Bool}
  %Equal.sym(Nat, LV.pos(8n, one), C.shift(128n, one), B.pos_shift(8n, one)) : {Nat.is_lt(Nat.add(FS.digits(one, cn8()), _), C.shift(129n, one)) == True{} : Bool}
  %Equal.sym(Nat, C.shift(129n, one), Nat.add(C.shift(128n, one), C.shift(128n, one)), Equal.sym(Nat, Nat.add(C.shift(128n, one), C.shift(128n, one)), C.shift(129n, one), shift_twice(128n, one))) : {Nat.is_lt(Nat.add(FS.digits(one, cn8()), C.shift(128n, one)), _) == True{} : Bool}
  I.lt_le_add(FS.digits(one, cn8()), C.shift(128n, one), C.shift(128n, one), C.shift(128n, one), I.lt_subst_r(FS.digits(one, cn8()), LV.pos(8n, one), C.shift(128n, one), B.pos_shift(8n, one), digits_lt(one, h1, 8n, cn8(), cn8_limbs(one, h1))), N.le_refl(C.shift(128n, one)))

# the fold bounds for n: 2 c < 2^256, (1 + c) c <= 4 2^256, 5 c + c <= 2^256
def cn_cc(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.add(FS.cn(one), FS.cn(one)), C.shift(256n, one)) == True{} : Bool}:
  +c = FS.cn(one)
  +s1 = I.lt_le_add(c, c, C.shift(129n, one), C.shift(129n, one), cn_lt(one, h1), N.lt_le(c, C.shift(129n, one), cn_lt(one, h1)))
  +s2 = I.lt_subst_r(Nat.add(c, c), Nat.add(C.shift(129n, one), C.shift(129n, one)), C.shift(130n, one), shift_twice(129n, one), s1)
  N.lt_trans(Nat.add(c, c), C.shift(130n, one), C.shift(256n, one), s2, shift_lt_k(one, h1, 130n, 256n, 125n, {==}))

def four_t(+one: Nat) -> {C.shift(258n, one) == Nat.mul(4n, C.shift(256n, one)) : Nat}:
  %Equal.sym(Nat, Nat.double(C.shift(256n, one)), Nat.add(C.shift(256n, one), C.shift(256n, one)), NA.double_self(C.shift(256n, one))) : {Nat.double(_) == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), 0n)))) : Nat}
  %Equal.sym(Nat, Nat.double(Nat.add(C.shift(256n, one), C.shift(256n, one))), Nat.add(Nat.add(C.shift(256n, one), C.shift(256n, one)), Nat.add(C.shift(256n, one), C.shift(256n, one))), NA.double_self(Nat.add(C.shift(256n, one), C.shift(256n, one)))) : {_ == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), 0n)))) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(256n, one), C.shift(256n, one)), Nat.add(C.shift(256n, one), C.shift(256n, one))), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))), NA.add_assoc(C.shift(256n, one), C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) : {_ == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), 0n)))) : Nat}
  %Equal.sym(Nat, Nat.add(C.shift(256n, one), 0n), C.shift(256n, one), NA.add_zero(C.shift(256n, one))) : {Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), _))) : Nat}
  {==}

def cn_hb1(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.mul(1n+FS.cn(one), FS.cn(one)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}:
  +c = FS.cn(one)
  +s1 = I.le_mul2(1n+c, c, C.shift(129n, one), C.shift(129n, one), N.lt_succ_le_succ(c, C.shift(129n, one), cn_lt(one, h1)), N.lt_le(c, C.shift(129n, one), cn_lt(one, h1)))
  +s2 = I.le_subst_r(Nat.mul(1n+c, c), Nat.mul(C.shift(129n, one), C.shift(129n, one)), C.shift(258n, one), shift_mul2(one, h1, 129n, 129n), s1)
  I.le_subst_r(Nat.mul(1n+c, c), C.shift(258n, one), Nat.mul(4n, C.shift(256n, one)), four_t(one), s2)

def six(+x: Nat) -> {Nat.add(Nat.mul(5n, x), x) == Nat.mul(6n, x) : Nat}:
  NA.add_comm(Nat.mul(5n, x), x)

def eight(+x: Nat) -> {Nat.mul(8n, x) == C.shift(3n, x) : Nat}:
  %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, _))))))) == Nat.double(Nat.double(Nat.double(x))) : Nat}
  %Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(Nat.double(_)) : Nat}
  %Equal.sym(Nat, Nat.double(Nat.add(x, x)), Nat.add(Nat.add(x, x), Nat.add(x, x)), NA.double_self(Nat.add(x, x))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(_) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))), NA.add_assoc(x, x, Nat.add(x, x))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(_) : Nat}
  %Equal.sym(Nat, Nat.double(Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(Nat.add(x, Nat.add(x, Nat.add(x, x))), Nat.add(x, Nat.add(x, Nat.add(x, x)))), NA.double_self(Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == _ : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(x, Nat.add(x, x))), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == _ : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.add(x, _) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, x, Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.add(x, Nat.add(x, _)) : Nat}
  {==}

def cn_hb2(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(Nat.mul(5n, FS.cn(one)), FS.cn(one)), C.shift(256n, one)) == True{} : Bool}:
  +c = FS.cn(one)
  +l = N.lt_le(c, C.shift(129n, one), cn_lt(one, h1))
  +s1 = I.le_add2(Nat.mul(5n, c), c, Nat.mul(5n, C.shift(129n, one)), C.shift(129n, one), I.le_mul_r(5n, c, C.shift(129n, one), l), l)
  +s2 = I.le_subst_r(Nat.add(Nat.mul(5n, c), c), Nat.add(Nat.mul(5n, C.shift(129n, one)), C.shift(129n, one)), Nat.mul(6n, C.shift(129n, one)), six(C.shift(129n, one)), s1)
  +s3 = N.le_trans(Nat.mul(6n, C.shift(129n, one)), Nat.mul(8n, C.shift(129n, one)), C.shift(132n, one), AR.mul_le(6n, 8n, C.shift(129n, one), {==}), I.le_subst_r(Nat.mul(8n, C.shift(129n, one)), C.shift(132n, one), C.shift(132n, one), {==}, N.eq_le(Nat.mul(8n, C.shift(129n, one)), C.shift(132n, one), eight(C.shift(129n, one)))))
  N.le_trans(Nat.add(Nat.mul(5n, c), c), Nat.mul(6n, C.shift(129n, one)), C.shift(256n, one), s2, N.le_trans(Nat.mul(6n, C.shift(129n, one)), C.shift(132n, one), C.shift(256n, one), s3, shift_le_k(132n, 256n, one, 124n, {==})))

# n = 1 + np, n + c = 2^256
def np(+one: Nat) -> Nat:
  Nat.sub(C.shift(256n, one), Nat.add(FS.cn(one), 1n))

def cn1_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(FS.cn(one), 1n), C.shift(256n, one)) == True{} : Bool}:
  +c = FS.cn(one)
  I.lt_succ_le(c, C.shift(256n, one), N.le_lt_trans(c, Nat.add(c, c), C.shift(256n, one), N.le_add_right(c, c), cn_cc(one, h1)))

def np_sum(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(FS.cn(one), 1n), np(one)) == C.shift(256n, one) : Nat}:
  N.sub_add(C.shift(256n, one), Nat.add(FS.cn(one), 1n), cn1_le(one, h1))

def hm_n(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(1n+np(one), FS.cn(one)) == C.shift(256n, one) : Nat}:
  %Equal.sym(Nat, C.shift(256n, one), Nat.add(Nat.add(FS.cn(one), 1n), np(one)), Equal.sym(Nat, Nat.add(Nat.add(FS.cn(one), 1n), np(one)), C.shift(256n, one), np_sum(one, h1))) : {Nat.add(1n+np(one), FS.cn(one)) == _ : Nat}
  %Equal.sym(Nat, 1n+np(one), Nat.add(np(one), 1n), SR.succ_add(1n, np(one))) : {Nat.add(_, FS.cn(one)) == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(np(one), 1n), FS.cn(one)), Nat.add(np(one), Nat.add(1n, FS.cn(one))), NA.add_assoc(np(one), 1n, FS.cn(one))) : {_ == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
  %Equal.sym(Nat, Nat.add(1n, FS.cn(one)), Nat.add(FS.cn(one), 1n), NA.add_comm(1n, FS.cn(one))) : {Nat.add(np(one), _) == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
  %Equal.sym(Nat, Nat.add(np(one), Nat.add(FS.cn(one), 1n)), Nat.add(FS.cn(one), Nat.add(np(one), 1n)), NA.add_swap(np(one), FS.cn(one), 1n)) : {_ == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(FS.cn(one), 1n), np(one)), Nat.add(FS.cn(one), Nat.add(1n, np(one))), NA.add_assoc(FS.cn(one), 1n, np(one))) : {Nat.add(FS.cn(one), Nat.add(np(one), 1n)) == _ : Nat}
  %Equal.sym(Nat, Nat.add(1n, np(one)), Nat.add(np(one), 1n), NA.add_comm(1n, np(one))) : {Nat.add(FS.cn(one), Nat.add(np(one), 1n)) == Nat.add(FS.cn(one), _) : Nat}
  {==}

def order_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.order(one) == 1n+np(one) : Nat}:
  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+np(one), FS.cn(one)), Equal.sym(Nat, Nat.add(1n+np(one), FS.cn(one)), C.shift(256n, one), hm_n(one, h1))) : {Nat.sub(_, FS.cn(one)) == 1n+np(one) : Nat}
  %Equal.sym(Nat, Nat.add(1n+np(one), FS.cn(one)), Nat.add(FS.cn(one), 1n+np(one)), NA.add_comm(1n+np(one), FS.cn(one))) : {Nat.sub(_, FS.cn(one)) == 1n+np(one) : Nat}
  N.add_sub_cancel(FS.cn(one), 1n+np(one))