F64sqr.ident: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as F64sqr
Lines 61-73 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend&start_line=61&end_line=73

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as SK

# N + q^2 == S0^2 + u 2^32
def 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)))

Uses (13):
  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.mul
  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/math/typed/f64sqk.bend&name=sqa
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend&name=usq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend&name=uw2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend&name=rearr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift