F64sqc.jfg: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
Lines 98-134 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend&start_line=98&end_line=134

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ2
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT

# the exponent step of sqn_c for any parity: 2a + p + s = 2b + q + 2171 with
# s <= 53, p <= 1, K <= 1022 and 2K + p = 2043 + u gives
# 2 ((a - b) - K) + 72 + s + u = 200 + q
def jfg(+a: Nat, +b: Nat, +sa: Nat, +p: Nat, +q: Nat, +K: Nat, +u: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), p), sa) == Nat.add(Nat.add(Nat.add(b, b), q), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hp: {Nat.is_le(p, 1n) == True{} : Bool}, +hK: {Nat.is_le(K, 1022n) == True{} : Bool}, +hKu: {Nat.add(Nat.add(K, K), p) == Nat.add(2043n, u) : Nat}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), K), Nat.sub(Nat.sub(a, b), K)), Nat.add(72n, Nat.add(sa, u))) == Nat.add(200n, q) : Nat}:
  +aa = Nat.add(a, a)
  +bb = Nat.add(b, b)
  +c54 = Nat.add(1n, 53n)
  +l0 = Equal.trans(Bool, Nat.is_le(Nat.add(bb, 2171n), Nat.add(Nat.add(bb, q), 2171n)), Nat.is_le(bb, Nat.add(bb, q)), True{}, FR.le_cancel_r(bb, Nat.add(bb, q), 2171n), N.le_add_right(bb, q))
  +l1 = L.subst(Nat, z => {Nat.is_le(Nat.add(bb, 2171n), z) == True{} : Bool}, Nat.add(Nat.add(bb, q), 2171n), Nat.add(Nat.add(aa, p), sa), Equal.sym(Nat, Nat.add(Nat.add(aa, p), sa), Nat.add(Nat.add(bb, q), 2171n), hEN2), l0)
  +l2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(aa, c54)) == True{} : Bool}, Nat.add(aa, Nat.add(p, sa)), Nat.add(Nat.add(aa, p), sa), Equal.sym(Nat, Nat.add(Nat.add(aa, p), sa), Nat.add(aa, Nat.add(p, sa)), NA.add_assoc(aa, p, sa)), N.le_add_left(Nat.add(p, sa), c54, aa, SQ2.le_add2(p, 1n, sa, 53n, hp, hsa)))
  +l3 = N.le_trans(Nat.add(bb, 2171n), Nat.add(Nat.add(aa, p), sa), Nat.add(aa, c54), l1, l2)
  +e4 = Equal.trans(Nat, Nat.add(Nat.add(bb, 2117n), c54), Nat.add(bb, Nat.add(2117n, c54)), Nat.add(bb, 2171n), NA.add_assoc(bb, 2117n, c54), Equal.cong(Nat, Nat, z => Nat.add(bb, z), Nat.add(2117n, c54), 2171n, {==}))
  +l4 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(aa, c54)) == True{} : Bool}, Nat.add(bb, 2171n), Nat.add(Nat.add(bb, 2117n), c54), Equal.sym(Nat, Nat.add(Nat.add(bb, 2117n), c54), Nat.add(bb, 2171n), e4), l3)
  +l5 = Equal.trans(Bool, Nat.is_le(Nat.add(bb, 2117n), aa), Nat.is_le(Nat.add(Nat.add(bb, 2117n), c54), Nat.add(aa, c54)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.add(bb, 2117n), c54), Nat.add(aa, c54)), Nat.is_le(Nat.add(bb, 2117n), aa), FR.le_cancel_r(Nat.add(bb, 2117n), aa, c54)), l4)
  +k3 = N.le_add_left(Nat.add(K, K), Nat.add(1022n, 1022n), bb, SQ2.le_add2(K, 1022n, K, 1022n, hK, hK))
  +k5 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, Nat.add(1022n, 1022n)), Nat.add(bb, 2117n), k3, N.le_add_left(Nat.add(1022n, 1022n), 2117n, bb, {==}))
  +k6 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, 2117n), aa, k5, l5)
  +eBK = Equal.trans(Nat, Nat.add(Nat.add(b, K), Nat.add(b, K)), Nat.add(b, Nat.add(K, Nat.add(b, K))), Nat.add(bb, Nat.add(K, K)), NA.add_assoc(b, K, Nat.add(b, K)), Equal.trans(Nat, Nat.add(b, Nat.add(K, Nat.add(b, K))), Nat.add(b, Nat.add(b, Nat.add(K, K))), Nat.add(bb, Nat.add(K, K)), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.add(K, Nat.add(b, K)), Nat.add(b, Nat.add(K, K)), NA.add_swap(K, b, K)), Equal.sym(Nat, Nat.add(bb, Nat.add(K, K)), Nat.add(b, Nat.add(b, Nat.add(K, K))), NA.add_assoc(b, b, Nat.add(K, K)))))
  +k7 = L.subst(Nat, z => {Nat.is_le(z, aa) == True{} : Bool}, Nat.add(bb, Nat.add(K, K)), Nat.add(Nat.add(b, K), Nat.add(b, K)), Equal.sym(Nat, Nat.add(Nat.add(b, K), Nat.add(b, K)), Nat.add(bb, Nat.add(K, K)), eBK), k6)
  +hbK = halve(Nat.add(b, K), a, k7)
  +hb = N.le_trans(b, Nat.add(b, K), a, N.le_add_right(b, K), hbK)
  +hK2 = RT.le_sub(K, b, a, L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, Nat.add(b, K), Nat.add(K, b), NA.add_comm(b, K), hbK))
  +D = Nat.sub(Nat.sub(a, b), K)
  +DD = Nat.add(D, D)
  +ea = Equal.trans(Nat, a, Nat.add(b, Nat.sub(a, b)), Nat.add(b, Nat.add(K, D)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, N.sub_add(a, b, hb)), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.sub(a, b), Nat.add(K, D), Equal.sym(Nat, Nat.add(K, D), Nat.sub(a, b), N.sub_add(Nat.sub(a, b), K, hK2))))
  +h2 = L.subst(Nat, z => {Nat.add(Nat.add(Nat.add(z, z), p), sa) == Nat.add(Nat.add(bb, q), 2171n) : Nat}, a, Nat.add(b, Nat.add(K, D)), ea, hEN2)
  +h3 = Equal.trans(Nat, Nat.add(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa))), Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(bb, Nat.add(q, 2171n)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa))), jperm(b, K, D, p, sa)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(Nat.add(bb, q), 2171n), Nat.add(bb, Nat.add(q, 2171n)), h2, NA.add_assoc(bb, q, 2171n)))
  +h4 = NR.add_cancel(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa)), Nat.add(q, 2171n), h3)
  +h5 = L.subst(Nat, z => {Nat.add(z, Nat.add(DD, sa)) == Nat.add(q, 2171n) : Nat}, Nat.add(Nat.add(K, K), p), Nat.add(2043n, u), hKu, h4)
  +W = Nat.add(u, Nat.add(DD, sa))
  +m1 = Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(2043n, W), Nat.add(1971n, Nat.add(72n, W)), NA.add_assoc(2043n, u, Nat.add(DD, sa)), {==})
  +m2 = Equal.trans(Nat, W, Nat.add(DD, Nat.add(u, sa)), Nat.add(DD, Nat.add(sa, u)), NA.add_swap(u, DD, sa), Equal.cong(Nat, Nat, z => Nat.add(DD, z), Nat.add(u, sa), Nat.add(sa, u), NA.add_comm(u, sa)))
  +m3 = Equal.trans(Nat, Nat.add(72n, W), Nat.add(72n, Nat.add(DD, Nat.add(sa, u))), Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Equal.cong(Nat, Nat, z => Nat.add(72n, z), W, Nat.add(DD, Nat.add(sa, u)), m2), NA.add_swap(72n, DD, Nat.add(sa, u)))
  +m4 = Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(72n, W)), Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), m1, Equal.cong(Nat, Nat, z => Nat.add(1971n, z), Nat.add(72n, W), Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), m3))
  +r1 = Equal.trans(Nat, Nat.add(q, 2171n), Nat.add(2171n, q), Nat.add(1971n, Nat.add(200n, q)), NA.add_comm(q, 2171n), {==})
  +fin = Equal.trans(Nat, Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(200n, q)), Equal.sym(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), m4), Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(q, 2171n), Nat.add(1971n, Nat.add(200n, q)), h5, r1))
  NR.add_cancel(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Nat.add(200n, q), fin)

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend&name=le_add2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=le_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=le_sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend&name=halve
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend&name=jperm