def ssh2
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:283
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
283def ssh2(+x: F.F64, +s: Bool, +e: Nat, +f: WU.U64, +z: Bool) -> {F.sq_sign(x, s, e, f, z) == SF.pick(F.F64, z, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))) : F.F64}:
284 match z:
285 case True{}:
286 Equal.trans(F.F64, F.sq_sign(x, s, e, f, True{}), x, SF.pick(F.F64, True{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), x, FR.pk_t(F.F64, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))))))
287 case False{}:
288 Equal.trans(F.F64, F.sq_sign(x, s, e, f, False{}), SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), SF.pick(F.F64, False{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), ssh3(e, f, s), Equal.sym(F.F64, SF.pick(F.F64, False{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), FR.pk_f(F.F64, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))))))