def sc_eq
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:75
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as F64sqa
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/src/math/natural.bend as M
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/lemmas/proofs/nat_algebra.bend as NA
75def sc_eq(+n: Nat, +j: Nat) -> {Nat.add(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), C.shift(j, M.isqrt(n))) == M.isqrt(C.shift(j, C.shift(j, n))) : Nat}:
76 Equal.trans(Nat, Nat.add(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), C.shift(j, M.isqrt(n))), Nat.add(C.shift(j, M.isqrt(n)), Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), M.isqrt(C.shift(j, C.shift(j, n))), NA.add_comm(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), C.shift(j, M.isqrt(n))), N.sub_add(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)), sc_lo(n, j)))