def sc_x
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:140
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
140def sc_x(+n: Nat, +j: Nat) -> {Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))) == Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)) : Bool}:
141 sc_x_c(n, j, Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n), {==})