1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/negate.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../../spec/crypto/secp256k1/field.bend as FS
5	import ../../../src/crypto/secp256k1/limbs.bend as L
6	import ../../lib/nat.bend as N
7	import ../../lib/logic.bend as Lg
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../math/natural/arith.bend as NR
10	import ../../math/typed/width.bend as WW
11	import ./semiring.bend as SR
12	import ./limbs.bend as LV
13	import ./ineq.bend as I
14	import ./bounds.bend as B
15	import ./reduce.bend as R
16	
17	# Complements and the borrow-free negation of src/crypto/secp256k1/limbs.bend:
18	# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16, and
19	# negraw(c, b) + b = 2 m for m = 2^256 - c (so a + negraw(c, b) is congruent
20	# to a - b), with 256 written as the symbolic 2^8 = C.shift(8n, one).
21	
22	def e255(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.sub(C.shift(8n, one), 1n) == 255n : Nat}:
23	  %Equal.sym(Nat, one, 1n, h1) : {Nat.sub(C.shift(8n, _), 1n) == 255n : Nat}
24	  {==}
25	
26	def bb_sq(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.mul(C.shift(8n, one), C.shift(8n, one)) == C.shift(16n, one) : Nat}:
27	  %Equal.sym(Nat, Nat.mul(C.shift(8n, one), C.shift(8n, one)), C.shift(8n, Nat.mul(one, C.shift(8n, one))), WW.shift_mul_l(8n, one, C.shift(8n, one))) : {_ == C.shift(16n, one) : Nat}
28	  %Equal.sym(Nat, Nat.mul(one, C.shift(8n, one)), C.shift(8n, one), LV.mul_one_l(one, h1, C.shift(8n, one))) : {C.shift(8n, _) == C.shift(16n, one) : Nat}
29	  %Equal.sym(Nat, C.shift(8n, C.shift(8n, one)), C.shift(16n, one), SR.shift_shift(8n, 8n, one)) : {_ == C.shift(16n, one) : Nat}
30	  {==}
31	
32	def bb_pos(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(1n, C.shift(8n, one)) == True{} : Bool}:
33	  %Equal.sym(Nat, one, 1n, h1) : {Nat.is_le(1n, C.shift(8n, _)) == True{} : Bool}
34	  {==}
35	
36	# (B - 1) + 1 = B
37	def pred_succ(+b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.add(Nat.sub(b, 1n), 1n) == b : Nat}:
38	  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), Nat.add(1n, Nat.sub(b, 1n)), NA.add_comm(Nat.sub(b, 1n), 1n)) : {_ == b : Nat}
39	  N.sub_add(b, 1n, h)
40	
41	# (B - 1) + (B - 1) B + 1 = B B
42	def digit_max(+b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n) == Nat.mul(b, b) : Nat}:
43	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n), Nat.add(Nat.sub(b, 1n), Nat.add(Nat.mul(Nat.sub(b, 1n), b), 1n)), NA.add_assoc(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b), 1n)) : {_ == Nat.mul(b, b) : Nat}
44	  %Equal.sym(Nat, Nat.add(Nat.mul(Nat.sub(b, 1n), b), 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b)), NA.add_comm(Nat.mul(Nat.sub(b, 1n), b), 1n)) : {Nat.add(Nat.sub(b, 1n), _) == Nat.mul(b, b) : Nat}
45	  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b))), Nat.add(Nat.add(Nat.sub(b, 1n), 1n), Nat.mul(Nat.sub(b, 1n), b)), Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(b, 1n), 1n), Nat.mul(Nat.sub(b, 1n), b)), Nat.add(Nat.sub(b, 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b))), NA.add_assoc(Nat.sub(b, 1n), 1n, Nat.mul(Nat.sub(b, 1n), b)))) : {_ == Nat.mul(b, b) : Nat}
46	  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), b, pred_succ(b, h)) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}
47	  %Equal.sym(Nat, b, Nat.mul(b, 1n), Equal.sym(Nat, Nat.mul(b, 1n), b, NA.mul_one(b))) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}
48	  %Equal.sym(Nat, Nat.mul(b, 1n), Nat.mul(1n, b), NA.mul_comm(b, 1n)) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}
49	  %Equal.sym(Nat, Nat.add(Nat.mul(1n, b), Nat.mul(Nat.sub(b, 1n), b)), Nat.mul(Nat.add(1n, Nat.sub(b, 1n)), b), Equal.sym(Nat, Nat.mul(Nat.add(1n, Nat.sub(b, 1n)), b), Nat.add(Nat.mul(1n, b), Nat.mul(Nat.sub(b, 1n), b)), NA.mul_add_right(1n, Nat.sub(b, 1n), b))) : {_ == Nat.mul(b, b) : Nat}
50	  %Equal.sym(Nat, Nat.add(1n, Nat.sub(b, 1n)), Nat.add(Nat.sub(b, 1n), 1n), NA.add_comm(1n, Nat.sub(b, 1n))) : {Nat.mul(_, b) == Nat.mul(b, b) : Nat}
51	  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), b, pred_succ(b, h)) : {Nat.mul(_, b) == Nat.mul(b, b) : Nat}
52	  {==}
53	
54	# x < 2^16: x div 256 < 256
55	def hi_byte_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(x, 256n), 256n) == True{} : Bool}:
56	  +bq = C.shift(8n, one)
57	  +hi = Nat.div(x, 256n)
58	  +le = I.le_subst_r(Nat.mul(hi, 256n), Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), x, Equal.sym(Nat, x, Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)), N.le_add_right(Nat.mul(hi, 256n), Nat.mod(x, 256n)))
59	  +le2 = I.le_subst_l(Nat.mul(hi, 256n), Nat.mul(hi, bq), x, Equal.cong(Nat, Nat, z => Nat.mul(hi, z), 256n, bq, Equal.sym(Nat, bq, 256n, LV.b8(one, h1))), le)
60	  +s1 = N.le_lt_trans(Nat.mul(hi, bq), x, C.shift(16n, one), le2, hx)
61	  +s2 = I.lt_subst_r(Nat.mul(hi, bq), C.shift(16n, one), Nat.mul(bq, bq), Equal.sym(Nat, Nat.mul(bq, bq), C.shift(16n, one), bb_sq(one, h1)), s1)
62	  +s3 = R.mul_lt_cancel(bq, hi, bq, s2, Nat.is_lt(hi, bq), {==})
63	  I.lt_subst_r(hi, bq, 256n, LV.b8(one, h1), s3)
64	
65	# (l + h B) + (h' B + l') = (l' + l) + (h' + h) B
66	def combine(+l: Nat, +h: Nat, +h2: Nat, +l2: Nat, +b: Nat) -> {Nat.add(Nat.add(l, Nat.mul(h, b)), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}:
67	  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.add(l, _), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
68	  %Equal.sym(Nat, Nat.add(l, Nat.mul(b, h)), Nat.add(Nat.mul(b, h), l), NA.add_comm(l, Nat.mul(b, h))) : {Nat.add(_, Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
69	  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(_, l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
70	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_assoc(Nat.mul(b, h), l, Nat.add(Nat.mul(b, h2), l2))) : {_ == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
71	  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), _) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
72	  %Equal.sym(Nat, Nat.add(l2, l), Nat.add(l, l2), NA.add_comm(l2, l)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(_, Nat.mul(Nat.add(h2, h), b)) : Nat}
73	  %Equal.sym(Nat, Nat.add(h2, h), Nat.add(h, h2), NA.add_comm(h2, h)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.mul(_, b)) : Nat}
74	  %Equal.sym(Nat, Nat.mul(Nat.add(h, h2), b), Nat.add(Nat.mul(h, b), Nat.mul(h2, b)), NA.mul_add_right(h, h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), _) : Nat}
75	  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(_, Nat.mul(h2, b))) : Nat}
76	  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), _)) : Nat}
77	  %Equal.sym(Nat, Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(l, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))), NA.add_assoc(l, l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}
78	  %Equal.sym(Nat, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(Nat.mul(b, h), Nat.add(l2, Nat.mul(b, h2))), NA.add_swap(l2, Nat.mul(b, h), Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, _) : Nat}
79	  %Equal.sym(Nat, Nat.add(l2, Nat.mul(b, h2)), Nat.add(Nat.mul(b, h2), l2), NA.add_comm(l2, Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, Nat.add(Nat.mul(b, h), _)) : Nat}
80	  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_swap(l, Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}
81	  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.mul(b, h), _) : Nat}
82	  {==}
83	
84	# comp1(x) + x + 1 = 2^16 for x < 2^16
85	def comp1_v(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), 1n) == C.shift(16n, one) : Nat}:
86	  +lo = Nat.mod(x, 256n)
87	  +hi = Nat.div(x, 256n)
88	  +hl = N.lt_succ_le(lo, 255n, NR.dm_lt(255n, x))
89	  +hh = N.lt_succ_le(hi, 255n, hi_byte_lt(one, h1, x, hx))
90	  %Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)) : {Nat.add(Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), _), 1n) == C.shift(16n, one) : Nat}
91	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n))), Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 256n)), combine(Nat.sub(255n, Nat.mod(x, 256n)), Nat.sub(255n, Nat.div(x, 256n)), Nat.div(x, 256n), Nat.mod(x, 256n), 256n)) : {Nat.add(_, 1n) == C.shift(16n, one) : Nat}
92	  %Equal.sym(Nat, 256n, C.shift(8n, one), Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1))) : {Nat.add(Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), _)), 1n) == C.shift(16n, one) : Nat}
93	  %Equal.sym(Nat, Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), 255n, N.sub_add(255n, Nat.mod(x, 256n), hl)) : {Nat.add(Nat.add(_, Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
94	  %Equal.sym(Nat, Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 255n, N.sub_add(255n, Nat.div(x, 256n), hh)) : {Nat.add(Nat.add(255n, Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
95	  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(_, Nat.mul(255n, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
96	  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
97	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(Nat.sub(C.shift(8n, one), 1n), C.shift(8n, one))), 1n), Nat.mul(C.shift(8n, one), C.shift(8n, one)), digit_max(C.shift(8n, one), bb_pos(one, h1))) : {_ == C.shift(16n, one) : Nat}
98	  bb_sq(one, h1)
99	
100	def comp1_o(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), one) == C.shift(16n, one) : Nat}:
101	  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(L.comp1(x), x), _) == C.shift(16n, one) : Nat}
102	  comp1_v(one, h1, x, hx)
103	
104	# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16
105	def comp_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {Nat.add(Nat.add(LV.ev(L.comp(xs)), LV.ev(xs)), one) == LV.pos(n, one) : Nat}:
106	  match n xs:
107	    case 0n Nil{}:
108	      {==}
109	    case 0n x <> t:
110	      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp(x <> t)), LV.ev(x <> t)), one) == LV.pos(0n, one) : Nat}, Lg.false_true(h))
111	    case 1n+k Nil{}:
112	      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp([])), LV.ev([])), one) == LV.pos(1n+k, one) : Nat}, Lg.false_true(h))
113	    case 1n+ +k +x <> +t:
114	      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
115	      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
116	      %Equal.sym(Nat, LV.pos(k, one), Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), LV.pos(k, one), comp_v(one, h1, k, t, ht))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(x, C.shift(16n, LV.ev(t)))), one) == C.shift(16n, _) : Nat}
117	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, LV.ev(t))), Nat.add(C.shift(16n, LV.ev(t)), x), NA.add_comm(x, C.shift(16n, LV.ev(t)))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), _), one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
118	      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(C.shift(16n, LV.ev(t)), x)), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), NA.add_assoc(L.comp1(x), C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))) : {Nat.add(_, one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
119	      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), one), Nat.add(L.comp1(x), Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)), NA.add_assoc(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)) : {_ == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
120	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one)), NA.add_assoc(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x), one)) : {Nat.add(L.comp1(x), _) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
121	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(x, one)), NA.add_assoc(C.shift(16n, LV.ev(t)), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), _)) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
122	      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _))) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
123	      %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one)), NA.add_assoc(LV.ev(L.comp(t)), LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == C.shift(16n, _) : Nat}
124	      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))), Nat.add(C.shift(16n, LV.ev(L.comp(t))), C.shift(16n, Nat.add(LV.ev(t), one))), WW.shift_add(16n, LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}
125	      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(t), one)), Nat.add(C.shift(16n, LV.ev(t)), C.shift(16n, one)), WW.shift_add(16n, LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}
126	      %Equal.sym(Nat, C.shift(16n, one), Nat.add(Nat.add(L.comp1(x), x), one), Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), C.shift(16n, one), comp1_o(one, h1, x, hx))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}
127	      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), Nat.add(L.comp1(x), Nat.add(x, one)), NA.add_assoc(L.comp1(x), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}
128	      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), _))) : Nat}
129	      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), Nat.add(one, x))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x))), NA.add_swap(C.shift(16n, LV.ev(t)), L.comp1(x), Nat.add(one, x))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}
130	      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), NA.add_swap(C.shift(16n, LV.ev(L.comp(t))), L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}
131	      {==}
132	
133	# ---- neg_raw(c, b) + b = m ----
134	
135	# b + c as 16 limbs, when b + c < 2^256
136	def bc_limbs(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.norm16(L.add(b, c))) == True{} : Bool}:
137	  B.carry_limbs(one, h1, 32n, 16n, L.add(b, c), 0n, {==})
138	
139	def bc_v(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>, +hbc: {Nat.is_lt(Nat.add(LV.ev(b), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.norm16(L.add(b, c))) == Nat.add(LV.ev(b), LV.ev(c)) : Nat}:
140	  +x = L.carry(32n, L.add(b, c), 0n)
141	  +ex = Equal.trans(Nat, LV.ev(x), LV.ev(L.add(b, c)), Nat.add(LV.ev(b), LV.ev(c)), LV.carry_v(32n, L.add(b, c), 0n), LV.add_v(b, c))
142	  +hx = I.lt_subst_l(Nat.add(LV.ev(b), LV.ev(c)), LV.ev(x), C.shift(256n, one), Equal.sym(Nat, LV.ev(x), Nat.add(LV.ev(b), LV.ev(c)), ex), hbc)
143	  %Equal.sym(Nat, LV.ev(L.take(16n, L.carry(32n, L.add(b, c), 0n))), LV.ev(L.carry(32n, L.add(b, c), 0n)), R.take_small(one, h1, L.carry(32n, L.add(b, c), 0n), hx)) : {_ == Nat.add(LV.ev(b), LV.ev(c)) : Nat}
144	  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(b, c), 0n)), Nat.add(LV.ev(b), LV.ev(c)), ex) : {_ == Nat.add(LV.ev(b), LV.ev(c)) : Nat}
145	  {==}
146	
147	# neg_raw(c, b) + b + c = 2^256
148	def neg_t(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>, +hbc: {Nat.is_lt(Nat.add(LV.ev(b), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), Nat.add(LV.ev(b), LV.ev(c))) == C.shift(256n, one) : Nat}:
149	  %Equal.sym(Nat, LV.ev(L.add(L.comp(L.norm16(L.add(b, c))), [1n])), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.add_v(L.comp(L.norm16(L.add(b, c))), [1n])) : {Nat.add(_, Nat.add(LV.ev(b), LV.ev(c))) == C.shift(256n, one) : Nat}
150	  %Equal.sym(Nat, Nat.add(LV.ev(b), LV.ev(c)), LV.ev(L.norm16(L.add(b, c))), Equal.sym(Nat, LV.ev(L.norm16(L.add(b, c))), Nat.add(LV.ev(b), LV.ev(c)), bc_v(one, h1, c, b, hbc))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), _) == C.shift(256n, one) : Nat}
151	  %Equal.sym(Nat, C.shift(256n, one), LV.pos(16n, one), Equal.sym(Nat, LV.pos(16n, one), C.shift(256n, one), B.pos16(one))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == _ : Nat}
152	  %Equal.sym(Nat, LV.pos(16n, one), Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), one), LV.pos(16n, one), comp_v(one, h1, 16n, L.norm16(L.add(b, c)), bc_limbs(one, h1, c, b)))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == _ : Nat}
153	  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), _) : Nat}
154	  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(1n, _)), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
155	  %Equal.sym(Nat, Nat.add(1n, 0n), 1n, {==}) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), _), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
156	  %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), 1n), LV.ev(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(1n, LV.ev(L.norm16(L.add(b, c))))), NA.add_assoc(LV.ev(L.comp(L.norm16(L.add(b, c)))), 1n, LV.ev(L.norm16(L.add(b, c))))) : {_ == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
157	  %Equal.sym(Nat, Nat.add(1n, LV.ev(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n), NA.add_comm(1n, LV.ev(L.norm16(L.add(b, c))))) : {Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), _) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
158	  %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n)), NA.add_assoc(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c))), 1n)) : {Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n)) == _ : Nat}
159	  {==}
160	
161	# neg_raw(c, b) + b = m, for b < m = 2^256 - c
162	def neg_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:
163	  +nb = LV.ev(L.neg_raw(c, b))
164	  +bv = LV.ev(b)
165	  +cv = LV.ev(c)
166	  +hbc = I.lt_subst_r(Nat.add(bv, cv), Nat.add(1n+mp, cv), C.shift(256n, one), hm, N.lt_add_r2(bv, 1n+mp, cv, hb))
167	  +e1 = Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(nb, Nat.add(bv, cv)), Nat.add(1n+mp, cv), NA.add_assoc(nb, bv, cv), Equal.trans(Nat, Nat.add(nb, Nat.add(bv, cv)), C.shift(256n, one), Nat.add(1n+mp, cv), neg_t(one, h1, c, b, hbc), Equal.sym(Nat, Nat.add(1n+mp, cv), C.shift(256n, one), hm)))
168	  NR.add_cancel(cv, Nat.add(nb, bv), 1n+mp, Equal.trans(Nat, Nat.add(cv, Nat.add(nb, bv)), Nat.add(Nat.add(nb, bv), cv), Nat.add(cv, 1n+mp), NA.add_comm(cv, Nat.add(nb, bv)), Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(1n+mp, cv), Nat.add(cv, 1n+mp), e1, NA.add_comm(1n+mp, cv))))
169	
170	def neg_vv(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, FS.value(one, c)) == C.shift(256n, one) : Nat}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:
171	  neg_v(one, h1, mp, c, Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), LV.ev_value(one, h1, c), hm), b, hb)
172	
173	# a + (m - b) = (a + m) - b, for b < m
174	def sub_mod(+mp: Nat, +a: Nat, +b: Nat, +nb: Nat, +hlt: {Nat.is_lt(b, 1n+mp) == True{} : Bool}, +hn: {Nat.add(nb, b) == 1n+mp : Nat}) -> {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), Nat.mod(b, 1n+mp)), 1n+mp) : Nat}:
175	  %Equal.sym(Nat, Nat.mod(b, 1n+mp), b, NR.mod_of(0n, mp, b, hlt)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), _), 1n+mp) : Nat}
176	  %Equal.sym(Nat, 1n+mp, Nat.add(nb, b), Equal.sym(Nat, Nat.add(nb, b), 1n+mp, hn)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, _), b), 1n+mp) : Nat}
177	  %Equal.sym(Nat, Nat.add(a, Nat.add(nb, b)), Nat.add(Nat.add(a, nb), b), Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(a, Nat.add(nb, b)), NA.add_assoc(a, nb, b))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
178	  %Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(b, Nat.add(a, nb)), NA.add_comm(Nat.add(a, nb), b)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
179	  %Equal.sym(Nat, Nat.sub(Nat.add(b, Nat.add(a, nb)), b), Nat.add(a, nb), N.add_sub_cancel(b, Nat.add(a, nb))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}
180	  {==}