def ssh3

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:276

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

276def ssh3(+e: Nat, +f: WU.U64, +s: Bool) -> {F.sq_pos(e, f, s) == 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}:
277  match s:
278    case True{}:
279      Equal.trans(F.F64, F.sq_pos(e, f, True{}), F.nan(), SF.pick(F.F64, True{}, 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{}, 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.nan(), FR.pk_t(F.F64, 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)))))
280    case False{}:
281      Equal.trans(F.F64, F.sq_pos(e, f, False{}), 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{}, 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, False{}, 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.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, 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)))))