def sc_high
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:84
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
84def sc_high(+n: Nat, +j: Nat) -> {C.high(j, M.isqrt(C.shift(j, C.shift(j, n)))) == M.isqrt(n) : Nat}:
85 Equal.trans(Nat, C.high(j, M.isqrt(C.shift(j, C.shift(j, n)))), C.high(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)))), M.isqrt(n), Equal.cong(Nat, Nat, z => C.high(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.high_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)))