def sc_low
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:87
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/math/typed/width.bend as WW
87def sc_low(+n: Nat, +j: Nat) -> {C.low(j, M.isqrt(C.shift(j, C.shift(j, n)))) == Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))) : Nat}:
88 Equal.trans(Nat, C.low(j, M.isqrt(C.shift(j, C.shift(j, n)))), C.low(j, 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.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), Equal.cong(Nat, Nat, z => C.low(j, z), M.isqrt(C.shift(j, C.shift(j, n))), 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))), Equal.sym(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))), sc_eq(n, j))), WW.low_u(j, Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), M.isqrt(n), sc_fit(n, j)))