def nf52
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:354
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
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/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/proofs/math/typed/f64adda.bend as AA
354def nf52(+y: F.F64, +hz: {Nat.is_eq(SF.efield(y), 0n) == False{} : Bool}) -> {C.fits(52n, SF.mant(y)) == False{} : Bool}:
355 AA.n52(SF.b2n(Bool.not(Nat.is_eq(SF.efield(y), 0n))), Equal.cong(Bool, Nat, b => SF.b2n(Bool.not(b)), Nat.is_eq(SF.efield(y), 0n), False{}, hz), SF.frac(y))