def rz_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:760

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

760def rz_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +zx: Bool, +hzx: {SF.is_zero(x) == zx : Bool}) -> {F.rm_z(x, y, zx) == RNs(x, y) : F.F64}:
761  match zx:
762    case True{}:
763      Equal.sym(F.F64, RNs(x, y), x, rm_zero(x, y, hzx, ok_zy(x, y, h), ok_fin(x, y, h)))
764    case False{}:
765      rfar_c(x, y, h, Nat.is_lt(F.dexp(x), F.dexp(y)), {==})