proofs/math/typed/f64sqr.bend source

proofs/math/typed/f64sqr.bend on the hub · documented module

import Baseimport ./f64light.bend as FLimport ./natlight.bend as NLimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/f64.bend as SFimport ../../../spec/math/w64.bend as SWimport ../../../src/math/f64.bend as Fimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../../src/math/natural.bend as Mimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/word.bend as WDimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/arith.bend as NRimport ../natural/sqrtn.bend as SQ2import ./width.bend as WWimport ./natcmp.bend as NCimport ./u32laws.bend as LWimport ./w64add.bend as WAimport ./w64mul.bend as W64Mimport ./w64sqrt.bend as W64Simport ./w64div.bend as W64Dimport ./w64est.bend as W64Eimport ./w64dm.bend as DMimport ./f64round.bend as FRimport ./f64rtools.bend as RTimport ./w64m128.bend as M128import ./f64sqa.bend as AQimport ./f64sqw.bend as QWimport ./f64sqk.bend as SKimport ./f64sqv.bend as QV# The F64 square root by one step of Zimmermann's SqrtRem (Karatsuba square# root; Bertot, Magaud and Zimmermann, "A proof of GMP square root", 2002)# with the exact remainder: for s = isqrt(nh), r = nh - s^2 and# q 2 s + u = r 2^32 (q < 2^32, u <= 2 s), S0 = s 2^32 + q satisfies# N + q^2 == S0^2 + u 2^32 for N = nh 2^64, so S0 - 2 <= isqrt(N) <= S0 and# the sign of u 2^32 - q^2 (then of the next remainders) picks the root and# its sticky bit.def v(+x: U32) -> Nat:  U32.to_nat(x)# x + b == y + a gives (a == b) == (x == y)def eqsh(+x: Nat, +b: Nat, +y: Nat, +a: Nat, +h: {Nat.add(x, b) == Nat.add(y, a) : Nat}) -> {Nat.is_eq(a, b) == Nat.is_eq(x, y) : Bool}:  +e1 = Equal.sym(Cmp, Nat.cmp(Nat.add(y, a), Nat.add(y, b)), Nat.cmp(a, b), NC.cmp_add(y, a, b))  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, Nat.add(y, b)), Nat.add(y, a), Nat.add(x, b), Equal.sym(Nat, Nat.add(x, b), Nat.add(y, a), h))  +e3 = NC.cmp_addr(x, y, b)  Equal.cong(Cmp, Bool, z => Cmp.is_eq(z), Nat.cmp(a, b), Nat.cmp(x, y), Equal.trans(Cmp, Nat.cmp(a, b), Nat.cmp(Nat.add(y, a), Nat.add(y, b)), Nat.cmp(x, y), e1, Equal.trans(Cmp, Nat.cmp(Nat.add(y, a), Nat.add(y, b)), Nat.cmp(Nat.add(x, b), Nat.add(y, b)), Nat.cmp(x, y), e2, e3)))# ((a + b) + d) + c == (a + (b + c)) + ddef rearr(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(Nat.add(a, b), d), c) == Nat.add(Nat.add(a, Nat.add(b, c)), d) : Nat}:  +e1 = NA.add_assoc(Nat.add(a, b), d, c)  +e2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(a, b), z), Nat.add(d, c), Nat.add(c, d), NA.add_comm(d, c))  +e3 = Equal.sym(Nat, Nat.add(Nat.add(Nat.add(a, b), c), d), Nat.add(Nat.add(a, b), Nat.add(c, d)), NA.add_assoc(Nat.add(a, b), c, d))  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, d), Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), NA.add_assoc(a, b, c))  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, b), d), c), Nat.add(Nat.add(a, b), Nat.add(d, c)), Nat.add(Nat.add(a, Nat.add(b, c)), d), e1, Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(d, c)), Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, Nat.add(b, c)), d), e2, Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(Nat.add(a, b), c), d), Nat.add(Nat.add(a, Nat.add(b, c)), d), e3, e4)))# N + q^2 == S0^2 + u 2^32def ident(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}:  +e0 = Equal.cong(Nat, Nat, z => Nat.mul(z, z), Nat.add(Q, C.shift(32n, s)), Nat.add(C.shift(32n, s), Q), NA.add_comm(Q, C.shift(32n, s)))  +e1 = SK.sqa(C.shift(32n, s), Q)  +e2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), z), Nat.mul(Q, Q)), Nat.add(Nat.mul(C.shift(32n, s), Q), Nat.mul(C.shift(32n, s), Q)), C.shift(32n, Nat.mul(Q, D)), SK.uw2(s, Q, D, hD))  +eS = Equal.trans(Nat, Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(C.shift(32n, s), Q), Nat.add(C.shift(32n, s), Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), e0, Equal.trans(Nat, Nat.mul(Nat.add(C.shift(32n, s), Q), Nat.add(C.shift(32n, s), Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(Nat.mul(C.shift(32n, s), Q), Nat.mul(C.shift(32n, s), Q))), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), e1, e2))  +f1 = Equal.sym(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), C.shift(32n, C.shift(32n, n)), SK.usq(s, rr, n, hn))  +f2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, z)), C.shift(32n, rr), Nat.add(Nat.mul(Q, D), U), Equal.sym(Nat, Nat.add(Nat.mul(Q, D), U), C.shift(32n, rr), hc))  +f3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), z), C.shift(32n, Nat.add(Nat.mul(Q, D), U)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U)), WW.shift_add(32n, Nat.mul(Q, D), U))  +eN = Equal.trans(Nat, C.shift(32n, C.shift(32n, n)), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), f1, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.add(Nat.mul(Q, D), U))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), f2, f3))  +g1 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(Q, Q)), C.shift(32n, C.shift(32n, n)), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), eN)  +g2 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, U)), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), eS)  Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), g1, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), rearr(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U), Nat.mul(Q, Q))), Equal.sym(Nat, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), g2)))def nn(+n: Nat) -> {C.shift(64n, n) == C.shift(32n, C.shift(32n, n)) : Nat}:  WW.shift_comp(32n, 32n, n)# N + q^2 == S0^2 + u 2^32, with N = nh 2^64def identN(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.add(C.shift(64n, n), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}:  Equal.trans(Nat, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(Q, Q)), C.shift(64n, n), C.shift(32n, C.shift(32n, n)), nn(n)), ident(s, rr, n, Q, U, D, hn, hD, hc))# N < (S0 + 1)^2, so isqrt(N) <= S0def lo_bound(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hU: {Nat.is_le(U, D) == True{} : Bool}) -> {Nat.is_lt(C.shift(64n, n), Nat.mul(1n+Nat.add(Q, C.shift(32n, s)), 1n+Nat.add(Q, C.shift(32n, s)))) == True{} : Bool}:  +a1 = N.le_add_right(C.shift(64n, n), Nat.mul(Q, Q))  +a2 = L.subst(Nat, z => {Nat.is_le(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc), a1)  +hPs = L.subst(Nat, z => {Nat.is_le(C.shift(32n, s), z) == True{} : Bool}, Nat.add(C.shift(32n, s), Q), Nat.add(Q, C.shift(32n, s)), NA.add_comm(C.shift(32n, s), Q), N.le_add_right(C.shift(32n, s), Q))  +a3 = N.le_trans(C.shift(32n, U), C.shift(32n, D), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), WW.shift_mono(32n, U, D, hU), L.subst(Nat, z => {Nat.is_le(C.shift(32n, z), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))) == True{} : Bool}, Nat.add(s, s), D, hD, L.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))) == True{} : Bool}, Nat.add(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.add(s, s)), Equal.sym(Nat, C.shift(32n, Nat.add(s, s)), Nat.add(C.shift(32n, s), C.shift(32n, s)), WW.shift_add(32n, s, s)), SQ2.le_add2(C.shift(32n, s), Nat.add(Q, C.shift(32n, s)), C.shift(32n, s), Nat.add(Q, C.shift(32n, s)), hPs, hPs))))  +a4 = N.le_trans(C.shift(64n, n), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), a2, N.le_add_left(C.shift(32n, U), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), a3))  +a5 = L.subst(Nat, z => {Nat.is_le(C.shift(64n, n), z) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), NA.add_comm(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), a4)  L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, 1n+Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.mul(1n+Nat.add(Q, C.shift(32n, s)), 1n+Nat.add(Q, C.shift(32n, s))), Equal.sym(Nat, Nat.mul(1n+Nat.add(Q, C.shift(32n, s)), 1n+Nat.add(Q, C.shift(32n, s))), 1n+Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), SQ2.succ_mul_succ(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), N.le_lt_trans(C.shift(64n, n), Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), 1n+Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), a5, N.lt_succ(Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))))))# S0 <= isqrt(N) + 2, for q < 2^32 and isqrt(N) >= 2^62def hi_bound(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hQ: {Nat.is_lt(Q, C.shift(32n, one)) == True{} : Bool}, +hT: {Nat.is_le(C.shift(62n, one), M.isqrt(C.shift(64n, n))) == True{} : Bool}) -> {Nat.is_le(Nat.add(Q, C.shift(32n, s)), Nat.add(M.isqrt(C.shift(64n, n)), 2n)) == True{} : Bool}:  +e64 = Equal.trans(Nat, Nat.mul(C.shift(32n, one), C.shift(32n, one)), C.shift(32n, C.shift(32n, Nat.mul(one, one))), C.shift(2n, C.shift(62n, one)), AQ.sh_sq(32n, one), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.mul(one, one))), C.shift(32n, C.shift(32n, one)), C.shift(2n, C.shift(62n, one)), Equal.cong(Nat, Nat, z => C.shift(32n, C.shift(32n, z)), Nat.mul(one, one), one, L.subst(Nat, o => {Nat.mul(o, o) == o : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})), Equal.trans(Nat, C.shift(32n, C.shift(32n, one)), C.shift(64n, one), C.shift(2n, C.shift(62n, one)), Equal.sym(Nat, C.shift(64n, one), C.shift(32n, C.shift(32n, one)), WW.shift_comp(32n, 32n, one)), WW.shift_comp(2n, 62n, one))))  +hq2 = N.le_trans(Nat.mul(Q, Q), Nat.mul(C.shift(32n, one), C.shift(32n, one)), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), AQ.sqmono(Q, C.shift(32n, one), N.lt_le(Q, C.shift(32n, one), hQ)), L.subst(Nat, z => {Nat.is_le(Nat.mul(C.shift(32n, one), C.shift(32n, one)), z) == True{} : Bool}, C.shift(2n, M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), SK.four(M.isqrt(C.shift(64n, n))), L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, M.isqrt(C.shift(64n, n)))) == True{} : Bool}, C.shift(2n, C.shift(62n, one)), Nat.mul(C.shift(32n, one), C.shift(32n, one)), Equal.sym(Nat, Nat.mul(C.shift(32n, one), C.shift(32n, one)), C.shift(2n, C.shift(62n, one)), e64), WW.shift_mono(2n, C.shift(62n, one), M.isqrt(C.shift(64n, n)), hT))))  +a1 = N.le_add_right(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U))  +a2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), z) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Equal.sym(Nat, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc)), a1)  +a3 = N.le_lt_trans(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))))), a2, N.lt_le_trans(Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))))), N.lt_add_r2(C.shift(64n, n), Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.mul(Q, Q), AQ.ilt(C.shift(64n, n))), N.le_add_left(Nat.mul(Q, Q), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), hq2)))  SK.k_hi_c(C.shift(64n, n), M.isqrt(C.shift(64n, n)), Nat.add(Q, C.shift(32n, s)), a3, Nat.is_le(Nat.add(Q, C.shift(32n, s)), Nat.add(M.isqrt(C.shift(64n, n)), 2n)), {==})def two62(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(2n, C.shift(62n, one)) == True{} : Bool}:  +h = L.subst(Nat, o => {Nat.is_le(o, C.shift(61n, one)) == True{} : Bool}, one, 1n, h1, WW.shift_ge(61n, one))  L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.add(C.shift(61n, one), C.shift(61n, one)), C.shift(62n, one), Equal.sym(Nat, C.shift(62n, one), Nat.add(C.shift(61n, one), C.shift(61n, one)), NA.double_self(C.shift(61n, one))), SQ2.le_add2(1n, C.shift(61n, one), 1n, C.shift(61n, one), h, h))# branch A: q^2 <= u 2^32 gives the root S0, exact iff q^2 == u 2^32def brA_T(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hU: {Nat.is_le(U, D) == True{} : Bool}, +hAB: {Nat.is_le(Nat.mul(Q, Q), C.shift(32n, U)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == Nat.add(Q, C.shift(32n, s)) : Nat}:  +a1 = N.le_add_left(Nat.mul(Q, Q), C.shift(32n, U), C.shift(64n, n), hAB)  +a2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), C.shift(32n, U))) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc), a1)  +a3 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), C.shift(32n, U))) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), NA.add_comm(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), a2)  +a4 = L.subst(Nat, z => {Nat.is_le(Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), z) == True{} : Bool}, Nat.add(C.shift(64n, n), C.shift(32n, U)), Nat.add(C.shift(32n, U), C.shift(64n, n)), NA.add_comm(C.shift(64n, n), C.shift(32n, U)), a3)  +hle = Equal.trans(Bool, Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), Nat.is_le(Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.add(C.shift(32n, U), C.shift(64n, n))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.add(C.shift(32n, U), C.shift(64n, n))), Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), NR.le_add_cancel(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n))), a4)  AQ.isqrt_char(C.shift(64n, n), Nat.add(Q, C.shift(32n, s)), hle, lo_bound(s, rr, n, Q, U, D, hn, hD, hc, hU))def brA_eq(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.is_eq(C.shift(32n, U), Nat.mul(Q, Q)) == Nat.is_eq(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)) : Bool}:  Equal.trans(Bool, Nat.is_eq(C.shift(32n, U), Nat.mul(Q, Q)), Nat.is_eq(C.shift(64n, n), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.is_eq(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), eqsh(C.shift(64n, n), Nat.mul(Q, Q), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U), identN(s, rr, n, Q, U, D, hn, hD, hc)), QW.eq_comm(C.shift(64n, n), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))))# branch B: q^2 > u 2^32, D = q^2 - u 2^32 > 0 and N + D == S0^2def brB_nd(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hBA: {Nat.is_lt(C.shift(32n, U), Nat.mul(Q, Q)) == True{} : Bool}) -> {Nat.add(C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))) == Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))) : Nat}:  +eD = N.sub_add(Nat.mul(Q, Q), C.shift(32n, U), N.lt_le(C.shift(32n, U), Nat.mul(Q, Q), hBA))  +e1 = L.subst(Nat, z => {Nat.add(C.shift(64n, n), z) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}, Nat.mul(Q, Q), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Equal.sym(Nat, Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.mul(Q, Q), eD), identN(s, rr, n, Q, U, D, hn, hD, hc))  +e2 = Equal.trans(Nat, Nat.add(C.shift(32n, U), Nat.add(C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.add(C.shift(64n, n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), NA.add_swap(C.shift(32n, U), C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Equal.trans(Nat, Nat.add(C.shift(64n, n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), e1, NA.add_comm(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U))))  NR.add_cancel(C.shift(32n, U), Nat.add(C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), e2)def brB_pos(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hBA: {Nat.is_lt(C.shift(32n, U), Nat.mul(Q, Q)) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))) == True{} : Bool}:  +eD = N.sub_add(Nat.mul(Q, Q), C.shift(32n, U), N.lt_le(C.shift(32n, U), Nat.mul(Q, Q), hBA))  +h = L.subst(Nat, z => {Nat.is_lt(C.shift(32n, U), z) == True{} : Bool}, Nat.mul(Q, Q), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Equal.sym(Nat, Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.mul(Q, Q), eD), hBA)  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))) == True{} : Bool}, C.shift(32n, U), Nat.add(C.shift(32n, U), 0n), Equal.sym(Nat, Nat.add(C.shift(32n, U), 0n), C.shift(32n, U), N.add_zero(C.shift(32n, U))), h)  Equal.trans(Bool, Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.is_lt(Nat.add(C.shift(32n, U), 0n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(C.shift(32n, U), 0n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), WW.lt_cancel_l(C.shift(32n, U), 0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), h2)# with S0 = 2 + S2 and S1 = 1 + S2: c = 2 S0 - 1 == 1 + 2 S1, S0^2 == c + S1^2, S1^2 == (c - 2) + S2^2def c_eq(+S2: Nat) -> {Nat.sub(Nat.add(2n+S2, 2n+S2), 1n) == 1n+Nat.add(1n+S2, 1n+S2) : Nat}:  Equal.cong(Nat, Nat, z => 1n+z, Nat.add(S2, 2n+S2), 1n+Nat.add(S2, 1n+S2), N.add_succ(S2, 1n+S2))def c2_eq(+S2: Nat) -> {Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n) == 1n+Nat.add(S2, S2) : Nat}:  +e1 = Equal.trans(Nat, Nat.add(S2, 2n+S2), 1n+Nat.add(S2, 1n+S2), 1n+1n+Nat.add(S2, S2), N.add_succ(S2, 1n+S2), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(S2, 1n+S2), 1n+Nat.add(S2, S2), N.add_succ(S2, S2)))  Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(S2, 2n+S2), 1n+1n+Nat.add(S2, S2), e1)def sq0_eq(+S2: Nat) -> {Nat.mul(2n+S2, 2n+S2) == Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)) : Nat}:  Equal.trans(Nat, Nat.mul(2n+S2, 2n+S2), 1n+Nat.add(Nat.add(1n+S2, 1n+S2), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), SQ2.succ_mul_succ(1n+S2, 1n+S2), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(1n+S2, 1n+S2)), 1n+Nat.add(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Equal.sym(Nat, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 1n+Nat.add(1n+S2, 1n+S2), c_eq(S2))))def sq1_eq(+S2: Nat) -> {Nat.mul(1n+S2, 1n+S2) == Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)) : Nat}:  Equal.trans(Nat, Nat.mul(1n+S2, 1n+S2), 1n+Nat.add(Nat.add(S2, S2), Nat.mul(S2, S2)), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), SQ2.succ_mul_succ(S2, S2), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S2, S2)), 1n+Nat.add(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Equal.sym(Nat, Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), 1n+Nat.add(S2, S2), c2_eq(S2))))# S1^2 + c == N + Ddef b_s1(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}) -> {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), Dx) : Nat}:  Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(C.shift(64n, n), Dx), NA.add_comm(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.mul(2n+S2, 2n+S2), Nat.add(C.shift(64n, n), Dx), Equal.sym(Nat, Nat.mul(2n+S2, 2n+S2), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), sq0_eq(S2)), Equal.sym(Nat, Nat.add(C.shift(64n, n), Dx), Nat.mul(2n+S2, 2n+S2), hnd)))# D <= c: the root is S1, exact iff D == cdef b1_T(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hpos: {Nat.is_lt(0n, Dx) == True{} : Bool}, +hs: {Nat.is_le(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == 1n+S2 : Nat}:  +e1 = b_s1(n, S2, Dx, hnd)  +a1 = N.le_add_left(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n), hs)  +a2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == True{} : Bool}, Nat.add(C.shift(64n, n), Dx), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Equal.sym(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Dx), e1), a1)  +a3 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n)), NA.add_comm(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == True{} : Bool}, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), NA.add_comm(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), a2))  +hle = Equal.trans(Bool, Nat.is_le(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n))), Nat.is_le(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), NR.le_add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), C.shift(64n, n))), a3)  +hlt = L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Dx), Nat.mul(2n+S2, 2n+S2), hnd, DM.lt_add_pos(C.shift(64n, n), Dx, hpos))  AQ.isqrt_char(C.shift(64n, n), 1n+S2, hle, hlt)def b1_eq(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}) -> {Nat.is_eq(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == Nat.is_eq(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)) : Bool}:  Equal.trans(Bool, Nat.is_eq(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx), Nat.is_eq(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.is_eq(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), QW.eq_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx), eqsh(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n), Dx, b_s1(n, S2, Dx, hnd)))# S2^2 + (c - 2) == N + (D - c) for c < Ddef b_s2(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}) -> {Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)) == Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) : Nat}:  +eD = N.sub_add(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.lt_le(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx, hb))  +e1 = L.subst(Nat, z => {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), z) : Nat}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), b_s1(n, S2, Dx, hnd))  +e2 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), NA.add_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), e1, NA.add_swap(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))))  +e3 = NR.add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e2)  Equal.trans(Nat, Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.trans(Nat, Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), Nat.mul(1n+S2, 1n+S2), NA.add_comm(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Equal.sym(Nat, Nat.mul(1n+S2, 1n+S2), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), sq1_eq(S2))), e3)# c < D: the root is S2 (it is at least S0 - 2), exact iff D - c == c - 2def b2_T(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}, +hge: {Nat.is_le(2n+S2, Nat.add(M.isqrt(C.shift(64n, n)), 2n)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == S2 : Nat}:  +eD = N.sub_add(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.lt_le(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx, hb))  +e1 = L.subst(Nat, z => {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), z) : Nat}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), b_s1(n, S2, Dx, hnd))  +e2 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), NA.add_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), e1, NA.add_swap(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))))  +e3 = NR.add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e2)  +hp = Equal.trans(Bool, Nat.is_lt(0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.is_lt(0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), WW.lt_cancel_l(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), z) == True{} : Bool}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), L.subst(Nat, z => {Nat.is_lt(z, Dx) == True{} : Bool}, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.add_zero(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), hb)))  +hlt = L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.mul(1n+S2, 1n+S2), Equal.sym(Nat, Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e3), DM.lt_add_pos(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), hp))  +hup = N.lt_succ_le(M.isqrt(C.shift(64n, n)), S2, AQ.isqrt_lt(C.shift(64n, n), 1n+S2, hlt))  +hdn = L.subst(Nat, z => {Nat.is_le(2n+S2, z) == True{} : Bool}, Nat.add(M.isqrt(C.shift(64n, n)), 2n), 2n+M.isqrt(C.shift(64n, n)), NA.add_comm(M.isqrt(C.shift(64n, n)), 2n), hge)  N.le_antisym(M.isqrt(C.shift(64n, n)), S2, hup, hdn)def b2_eq(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}) -> {Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == Nat.is_eq(Nat.mul(S2, S2), C.shift(64n, n)) : Bool}:  Equal.trans(Bool, Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.is_eq(Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.is_eq(Nat.mul(S2, S2), C.shift(64n, n)), QW.eq_comm(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), eqsh(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), b_s2(n, S2, Dx, hnd, hb)))# roundPackToF64 of the root with its sticky bit is the spec's rounddef fin_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +t: WU.U64, +st: Bool, +ht: {SW.value(t) == M.isqrt(C.shift(64n, SW.value(nh))) : Nat}, +hst: {st == Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))) : Bool}) -> {F.sq_fin(e, t, st) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +ev = Equal.trans(Nat, SW.value(X.or_bit(t, st)), SW.jam(SW.value(t), SF.b2n(st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), FL.orv(t, st), Equal.trans(Nat, SW.jam(SW.value(t), SF.b2n(st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Equal.cong(Nat, Nat, z => SW.jam(z, SF.b2n(st)), SW.value(t), M.isqrt(C.shift(64n, SW.value(nh))), ht), Equal.cong(Bool, Nat, z => SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(z)), st, Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))), hst)))  +s63 = Equal.trans(Bool, C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(63n, one)), True{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(63n, one)), C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), FR.lt_fit(63n, one, h1, M.isqrt(C.shift(64n, SW.value(nh))))), N.lt_le_trans(M.isqrt(C.shift(64n, SW.value(nh))), SW.value(WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}), C.shift(63n, one), QV.s_hi(one, h1, nh, h62, h60, WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}, QV.r0_v(one, h1, nh, h62, h60), QV.r0_hi(one, h1, nh, h62, h60)), QV.r0_63(one, h1, nh, h62, h60, WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}, QV.r0_v(one, h1, nh, h62, h60), QV.r0_hi(one, h1, nh, h62, h60))))  +s62 = Equal.trans(Bool, C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one)), False{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one)), C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), FR.lt_fit(62n, one, h1, M.isqrt(C.shift(64n, SW.value(nh))))), N.le_not_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one), QV.s62(one, h1, nh, h62, h60)))  +j63 = Equal.trans(Bool, C.fits(63n, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))))))), C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), True{}, RT.jam_fits(62n, M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), s63)  +j62 = Equal.trans(Bool, C.fits(62n, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))))))), C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), False{}, RT.jam_fits(61n, M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), s62)  +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), SW.value(X.or_bit(t, st)), Equal.sym(Nat, SW.value(X.or_bit(t, st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), ev), j63)  +h62b = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), SW.value(X.or_bit(t, st)), Equal.sym(Nat, SW.value(X.or_bit(t, st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), ev), j62)  +r1 = FR.round_pack(False{}, e, X.or_bit(t, st), x, hx, h62b, h63)  Equal.trans(F.F64, F.sq_fin(e, t, st), SF.round(False{}, SW.value(X.or_bit(t, st)), x), SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x), r1, Equal.cong(Nat, F.F64, z => SF.round(False{}, z, x), SW.value(X.or_bit(t, st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), ev))def sticky_eq(+a: Bool, +b: Bool, +h: {a == b : Bool}) -> {Bool.not(a) == Bool.not(b) : Bool}:  Equal.cong(Bool, Bool, z => Bool.not(z), a, b, h)def s0v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32) -> {SW.value(WU.U64{q, X.lo(X.isqrt(nh))}) == Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))) : Nat}:  Equal.cong(Nat, Nat, z => Nat.add(v(q), C.shift(32n, z)), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), QV.s_v(one, h1, nh, h62, h60))def bv_q(+q: U32) -> {SW.value(X.mul32(q, q)) == Nat.mul(v(q), v(q)) : Nat}:  W64M.mul32_value(q, q)# S0 < 2^63: q < 2^32 and s + 1 <= 2^31def s0_63(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one)) == True{} : Bool}:  +l1 = N.lt_le_trans(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), N.lt_add_r2(v(q), C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh))), hQ), N.le_refl(Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh))))))  +e1 = Equal.sym(Nat, C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), WW.shift_add(32n, one, M.isqrt(SW.value(nh))))  +l0 = L.subst(Nat, o => {Nat.is_le(Nat.add(o, M.isqrt(SW.value(nh))), C.shift(31n, one)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le_succ(M.isqrt(SW.value(nh)), C.shift(31n, one), QV.iv31(one, h1, nh, h62, h60)))  +l2 = WW.shift_mono(32n, Nat.add(one, M.isqrt(SW.value(nh))), C.shift(31n, one), l0)  +l3 = L.subst(Nat, z => {Nat.is_le(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), z) == True{} : Bool}, C.shift(32n, C.shift(31n, one)), C.shift(63n, one), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, C.shift(31n, one)), WW.shift_comp(32n, 31n, one)), l2)  N.lt_le_trans(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), l1, L.subst(Nat, z => {Nat.is_le(z, C.shift(63n, one)) == True{} : Bool}, C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), e1), l3))# 2 <= S0 (S0 >= isqrt(N) >= 2^62)def s0_2(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {Nat.is_le(2n, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))) == True{} : Bool}:  +hT = N.lt_succ_le(M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), AQ.isqrt_lt(C.shift(64n, SW.value(nh)), 1n+Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), lo_bound(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hU)))  N.le_trans(2n, C.shift(62n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), two62(one, h1), N.le_trans(C.shift(62n, one), M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), QV.s62(one, h1, nh, h62, h60), hT))def hS(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))) == 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n) : Nat}:  Equal.sym(Nat, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), N.sub_add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n, s0_2(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))def cw_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n) : Nat}:  +l63 = s0_63(one, h1, nh, h62, h60, q, hQ)  +f = WW.fits_one(64n, one, h1, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), z) == True{} : Bool}, Nat.add(C.shift(63n, one), C.shift(63n, one)), C.shift(64n, one), Equal.sym(Nat, C.shift(64n, one), Nat.add(C.shift(63n, one), C.shift(63n, one)), NA.double_self(C.shift(63n, one))), N.lt_le_trans(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(C.shift(63n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(C.shift(63n, one), C.shift(63n, one)), N.lt_add_r2(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), l63), L.subst(Nat, z => {Nat.is_le(Nat.add(C.shift(63n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), z) == True{} : Bool}, Nat.add(C.shift(63n, one), C.shift(63n, one)), Nat.add(C.shift(63n, one), C.shift(63n, one)), {==}, N.le_add_left(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), C.shift(63n, one), N.lt_le(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), l63))))))  +fs = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Equal.trans(Nat, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q))), Equal.cong(Nat, Nat, z => Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), z), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q)))), f)  +ea = Equal.trans(Nat, SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), M128.add64_exact(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}, fs), Equal.trans(Nat, Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), z), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q))))  +h1l = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Equal.sym(Nat, SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), ea), N.le_trans(1n, 2n, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), {==}, N.le_trans(2n, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), s0_2(one, h1, nh, h62, h60, q, u, hc, hU, hQ), N.le_add_right(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))))))  +es = Equal.trans(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), 1n), Nat.sub(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), 1n), WA.sub_value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}, h1l), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), ea))  Equal.trans(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), 1n), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), es, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, z), 1n), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))def le_ba(+q: U32, +u: U32) -> {X.le(X.mul32(q, q), WU.U64{0, u}) == Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))) : Bool}:  Equal.trans(Bool, X.le(X.mul32(q, q), WU.U64{0, u}), Nat.is_le(SW.value(X.mul32(q, q)), SW.value(WU.U64{0, u})), Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), WA.le_value(X.mul32(q, q), WU.U64{0, u}), Equal.cong(Nat, Bool, z => Nat.is_le(z, C.shift(32n, v(u))), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))def eq_ab(+q: U32, +u: U32) -> {X.eq(WU.U64{0, u}, X.mul32(q, q)) == Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) : Bool}:  Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(SW.value(WU.U64{0, u}), SW.value(X.mul32(q, q))), Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))), WA.eq_value(WU.U64{0, u}, X.mul32(q, q)), Equal.cong(Nat, Bool, z => Nat.is_eq(C.shift(32n, v(u)), z), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))# branch A: the root S0def brA_w(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hge: {X.le(X.mul32(q, q), WU.U64{0, u}) == True{} : Bool}) -> {F.sq_rem(e, WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{0, u}, X.mul32(q, q), True{}) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +hAB = Equal.trans(Bool, Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), X.le(X.mul32(q, q), WU.U64{0, u}), True{}, Equal.sym(Bool, X.le(X.mul32(q, q), WU.U64{0, u}), Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), le_ba(q, u)), hge)  +eT = brA_T(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hU, hAB)  +ht = Equal.trans(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), M.isqrt(C.shift(64n, SW.value(nh))), s0v(one, h1, nh, h62, h60, q), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), eT))  +e1 = Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))), Nat.is_eq(Nat.mul(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), C.shift(64n, SW.value(nh))), eq_ab(q, u), brA_eq(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc))  +e2 = Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(Nat.mul(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), C.shift(64n, SW.value(nh))), Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))), e1, Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.mul(z, z), C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), M.isqrt(C.shift(64n, SW.value(nh))), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), eT)))  fin_v(one, h1, nh, h62, h60, e, x, hx, WU.U64{q, X.lo(X.isqrt(nh))}, Bool.not(X.eq(WU.U64{0, u}, X.mul32(q, q))), ht, sticky_eq(X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))), e2))def one_le(+x: Nat, +h: {Nat.is_le(2n, x) == True{} : Bool}) -> {Nat.is_le(1n, x) == True{} : Bool}:  N.le_trans(1n, 2n, x, {==}, h)def dw_value(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}) -> {SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})) == Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))) : Nat}:  +h = L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(u)), z) == True{} : Bool}, Nat.mul(v(q), v(q)), SW.value(X.mul32(q, q)), Equal.sym(Nat, SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)), N.lt_le(C.shift(32n, v(u)), Nat.mul(v(q), v(q)), hBA))  Equal.trans(Nat, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(SW.value(X.mul32(q, q)), SW.value(WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), WA.sub_value(X.mul32(q, q), WU.U64{0, u}, h), Equal.cong(Nat, Nat, z => Nat.sub(z, C.shift(32n, v(u))), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))def s0w_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {SW.value(WU.U64{q, X.lo(X.isqrt(nh))}) == 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n) : Nat}:  Equal.trans(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0v(one, h1, nh, h62, h60, q), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ))def hnd_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}) -> {Nat.add(C.shift(64n, SW.value(nh)), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))) == Nat.mul(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)) : Nat}:  Equal.trans(Nat, Nat.add(C.shift(64n, SW.value(nh)), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), Nat.mul(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.mul(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), brB_nd(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hBA), Equal.cong(Nat, Nat, z => Nat.mul(z, z), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))def sm_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}) -> {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)) : Bool}:  Equal.trans(Bool, X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.is_le(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), WA.le_value(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Equal.trans(Bool, Nat.is_le(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), Equal.cong(Nat, Bool, z => Nat.is_le(z, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), z), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ))))# branch B, D <= c: the root S0 - 1def brB1_w(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}, +hs: {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == True{} : Bool}) -> {F.sq_d1(e, WU.U64{q, X.lo(X.isqrt(nh))}, X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), True{}) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +hs2 = Equal.trans(Bool, Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), True{}, Equal.sym(Bool, X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), sm_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), hs)  +eT = b1_T(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA), brB_pos(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hBA), hs2)  +h1l = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), N.le_trans(1n, 2n, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), {==}, N.le_add_right(2n, Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))))  +ev = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0})), Nat.sub(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 1n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), WA.sub_value(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0}, h1l), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))  +ht = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0})), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), ev, Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT))  +e1 = Equal.trans(Bool, X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), WA.eq_value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Equal.trans(Bool, Nat.is_eq(SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), Equal.cong(Nat, Bool, z => Nat.is_eq(z, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), z), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA))))  +e2 = Equal.trans(Bool, X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), Nat.is_eq(Nat.mul(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), e1, b1_eq(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)))  +e3 = Equal.trans(Bool, X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(Nat.mul(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))), e2, Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.mul(z, z), C.shift(64n, SW.value(nh))), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT)))  fin_v(one, h1, nh, h62, h60, e, x, hx, X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0}), Bool.not(X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u}))), ht, sticky_eq(X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))), e3))# branch B, D > c: the root S0 - 2def brB2_w(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}, +hs: {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == False{} : Bool}) -> {F.sq_d2(e, WU.U64{q, X.lo(X.isqrt(nh))}, X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +hs2 = Equal.trans(Bool, Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), False{}, Equal.sym(Bool, X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), sm_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), hs)  +hb = N.not_le_lt(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), hs2)  +hge = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(C.shift(64n, SW.value(nh))), 2n)) == True{} : Bool}, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ), hi_bound(one, h1, M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hQ, QV.s62(one, h1, nh, h62, h60)))  +eT = b2_T(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA), hb, hge)  +h2l = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), N.le_add_right(2n, Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)))  +ev = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0})), Nat.sub(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), WA.sub_value(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0}, h2l), Equal.trans(Nat, Nat.sub(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n), Nat.sub(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 0n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Equal.cong(Nat, Nat, z => Nat.sub(z, 2n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), N.sub_zero(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))))  +ht = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0})), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), ev, Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT))  +c2l0 = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, 1n+Nat.add(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Equal.sym(Nat, Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 1n+Nat.add(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), c_eq(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))), N.le_add_right(2n, Nat.add(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))))  +c2l = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Equal.sym(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), c2l0)  +e21 = Equal.trans(Nat, SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), Nat.sub(SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), 2n), Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), WA.sub_value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}, c2l), Equal.cong(Nat, Nat, z => Nat.sub(z, 2n), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))  +hcd = L.subst(Nat, z => {Nat.is_le(z, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))) == True{} : Bool}, Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Equal.sym(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), L.subst(Nat, z => {Nat.is_le(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), z) == True{} : Bool}, Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Equal.sym(Nat, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), N.lt_le(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hb)))  +e22 = Equal.trans(Nat, SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), WA.sub_value(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), hcd), Equal.trans(Nat, Nat.sub(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), Equal.cong(Nat, Nat, z => Nat.sub(z, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), Equal.cong(Nat, Nat, z => Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), z), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ))))  +e1 = Equal.trans(Bool, X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n))), WA.eq_value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Equal.trans(Bool, Nat.is_eq(SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n))), Equal.cong(Nat, Bool, z => Nat.is_eq(z, SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), e21), Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), z), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), e22)))  +e2 = Equal.trans(Bool, X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n))), Nat.is_eq(Nat.mul(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), e1, b2_eq(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA), hb))  +e3 = Equal.trans(Bool, X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(Nat.mul(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))), e2, Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.mul(z, z), C.shift(64n, SW.value(nh))), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT)))  fin_v(one, h1, nh, h62, h60, e, x, hx, X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0}), Bool.not(X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), ht, sticky_eq(X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh))), e3))def d1_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}, +sm: Bool, +hsm: {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == sm : Bool}) -> {F.sq_d1(e, WU.U64{q, X.lo(X.isqrt(nh))}, X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), sm) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  match sm:    case True{}:      brB1_w(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, hBA, hsm)    case False{}:      brB2_w(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, hBA, hsm)def rem_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +g: Bool, +hg: {X.le(X.mul32(q, q), WU.U64{0, u}) == g : Bool}) -> {F.sq_rem(e, WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{0, u}, X.mul32(q, q), g) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  match g:    case True{}:      brA_w(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, hg)    case False{}:      +h0 = Equal.trans(Bool, Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), X.le(X.mul32(q, q), WU.U64{0, u}), False{}, Equal.sym(Bool, X.le(X.mul32(q, q), WU.U64{0, u}), Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), le_ba(q, u)), hg)      d1_v(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, N.not_le_lt(Nat.mul(v(q), v(q)), C.shift(32n, v(u)), h0), X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), {==})def qu_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {F.sq_qu(e, X.lo(X.isqrt(nh)), q, u) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  rem_v(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, X.le(X.mul32(q, q), WU.U64{0, u}), {==})def shl_le_c(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(C.shift(k, a), C.shift(k, b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(a, b) == c : Bool}) -> {c == True{} : Bool}:  match c:    case True{}:      {==}    case False{}:      +h2 = WW.shift_lt(k, b, a, N.not_le_lt(a, b, hc))      Empty.absurd({False{} == True{} : Bool}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(C.shift(k, b), C.shift(k, a)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(k, b), C.shift(k, a)), True{}, h2), N.le_not_lt(C.shift(k, b), C.shift(k, a), h))))# shift(k, a) <= shift(k, b) gives a <= bdef shl_le_inv(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(C.shift(k, a), C.shift(k, b)) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:  shl_le_c(k, a, b, h, Nat.is_le(a, b), {==})# x / D * D + x mod D == x and x mod D < Ddef dmq(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.add(Nat.mul(Nat.div(x, D), D), Nat.mod(x, D)) == x : Nat}:  NL.dmq(x, D, hD)def dml(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.is_lt(Nat.mod(x, D), D) == True{} : Bool}:  NL.dml(x, D, hD)# q < 2^32: the digit as it isdef cl_t(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hu: {v(uu) == Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == True{} : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, True{}) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +eq1 = Equal.trans(Nat, v(X.lo(qq)), SW.value(qq), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), W64E.lo_hi0(qq, hz), hq)  +hc = Equal.trans(Nat, Nat.add(Nat.mul(v(X.lo(qq)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.trans(Nat, Nat.add(Nat.mul(v(X.lo(qq)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), v(X.lo(qq)), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), eq1), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), z), v(uu), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hu)), dmq(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60)))  +hU = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu), Equal.sym(Nat, v(uu), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hu), N.lt_le(Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), dml(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60))))  +hQ = WW.lt_one(32n, one, h1, v(X.lo(qq)), LW.vb(X.lo(qq)))  qu_v(one, h1, nh, h62, h60, e, x, hx, X.lo(qq), uu, hc, hU, hQ)# q = 2^32 (r = 2 s): taken as 2^32 - 1 with u = 2 s# over an open all-ones word o: v(4294967295) would be expanded in unarydef cl_f_o(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == False{} : Bool}, +o: U32, +po: {o == U32{WD.mask(32n, 32n)} : U32}) -> {F.sq_qu(e, X.lo(X.isqrt(nh)), o, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +e1 = Equal.trans(Nat, 1n+v(o), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, o, po), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))  +hQ = L.subst(Nat, z => {Nat.is_lt(v(o), z) == True{} : Bool}, 1n+v(o), C.shift(32n, one), e1, N.lt_succ(v(o)))  +eU = QV.dw_v(one, h1, nh, h62, h60)  +hhi = WA.pos_ne(v(X.hi(qq)), Equal.trans(Bool, Nat.is_eq(v(X.hi(qq)), 0n), U32.is_zero(X.hi(qq)), False{}, Equal.sym(Bool, U32.is_zero(X.hi(qq)), Nat.is_eq(v(X.hi(qq)), 0n), LW.zero_nat(X.hi(qq))), hz))  +g1 = N.le_trans(C.shift(32n, one), C.shift(32n, v(X.hi(qq))), SW.value(qq), WW.shift_mono(32n, one, v(X.hi(qq)), L.subst(Nat, z => {Nat.is_le(z, v(X.hi(qq))) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), hhi)), L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(X.hi(qq))), z) == True{} : Bool}, Nat.add(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), SW.value(qq), Equal.trans(Nat, Nat.add(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), Nat.add(v(X.lo(qq)), C.shift(32n, v(X.hi(qq)))), SW.value(qq), NA.add_comm(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), Equal.sym(Nat, SW.value(qq), Nat.add(v(X.lo(qq)), C.shift(32n, v(X.hi(qq)))), WA.val_eta(qq))), N.le_add_right(C.shift(32n, v(X.hi(qq))), v(X.lo(qq)))))  +hqD = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(qq), Equal.sym(Nat, SW.value(qq), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hq), QV.dq_le(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60)))  +g2 = SK.qb(one, h1, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(qq), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), hqD, QV.r_le(one, h1, nh, h62, h60), QV.d_pos(one, h1, nh, h62, h60))  +eq1 = N.le_antisym(SW.value(qq), C.shift(32n, one), g2, g1)  +g3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, SW.value(qq), C.shift(32n, one), eq1, hqD)  +eP = Equal.trans(Nat, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), NA.mul_comm(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))))  +g4 = L.subst(Nat, z => {Nat.is_le(z, C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), eP, g3)  +g5 = N.le_antisym(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.r_le(one, h1, nh, h62, h60), shl_le_inv(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), g4))  +hc0 = Equal.trans(Nat, Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), NA.add_comm(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.trans(Nat, Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), 1n+v(o), C.shift(32n, one), e1), Equal.trans(Nat, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), eP, Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), g5)))))  +hc = Equal.trans(Nat, Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), eU), hc0)  +hU = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Equal.sym(Nat, v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), eU), N.le_refl(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))  qu_v(one, h1, nh, h62, h60, e, x, hx, o, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), hc, hU, hQ)def cl_f(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == False{} : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, False{}) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  cl_f_o(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hz, 4294967295, {==})def cl_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hu: {v(uu) == Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +sm: Bool, +hsm: {U32.is_zero(X.hi(qq)) == sm : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, sm) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  match sm:    case True{}:      cl_t(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hu, hsm)    case False{}:      cl_f(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hsm)def div_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, p: WU.U64 & U32, +hq: {SW.value(X.fst_q(p)) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hu: {v(X.snd_r(p)) == Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}) -> {F.sq_div(e, X.lo(X.isqrt(nh)), p) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  match p:    case Tuple{+qq, +uu}:      cl_v(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hu, U32.is_zero(X.hi(qq)), {==})# the F64 root: roundPackToF64 of isqrt(nh 2^64) with its sticky bitdef sqr_root_v(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}) -> {F.sq_root(e, nh) == SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), x) : F.F64}:  +hu = Equal.trans(Nat, v(X.snd_r(X.div32(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), Nat.mod(SW.value(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), W64D.div32_rem(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), QV.dw_nz(one, h1, nh, h62, h60)), Equal.trans(Nat, Nat.mod(SW.value(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), QV.lo_w(one, h1, nh, h62, h60)), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.dw_v(one, h1, nh, h62, h60))))  div_v(one, h1, nh, h62, h60, e, x, hx, X.div32(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), QV.q_v(one, h1, nh, h62, h60), hu)