def sc_lo

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:68

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/logic.bend as L

68# isqrt(n * 4^j) lies in [isqrt(n) * 2^j, (isqrt(n) + 1) * 2^j)
69def sc_lo(+n: Nat, +j: Nat) -> {Nat.is_le(C.shift(j, M.isqrt(n)), M.isqrt(C.shift(j, C.shift(j, n)))) == True{} : Bool}:
70  isqrt_ge(C.shift(j, C.shift(j, n)), C.shift(j, M.isqrt(n)), L.subst(Nat, z => {Nat.is_le(z, C.shift(j, C.shift(j, n))) == True{} : Bool}, C.shift(j, C.shift(j, Nat.mul(M.isqrt(n), M.isqrt(n)))), Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), Equal.sym(Nat, Nat.mul(C.shift(j, M.isqrt(n)), C.shift(j, M.isqrt(n))), C.shift(j, C.shift(j, Nat.mul(M.isqrt(n), M.isqrt(n)))), sh_sq(j, M.isqrt(n))), le_sh2(j, Nat.mul(M.isqrt(n), M.isqrt(n)), n, isl(n))))