def fz_c

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

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

536def fz_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +zx: Bool, +hzx: {SF.is_zero(x) == zx : Bool}) -> {F.fmod_z(x, y, zx) == FM(x, y) : F.F64}:
537  match zx:
538    case True{}:
539      Equal.sym(F.F64, FM(x, y), x, fm_zero(x, y, hzx, ok_zy(x, y, h), ok_fin(x, y, h)))
540    case False{}:
541      ff_c(x, y, h, Nat.is_lt(F.dexp(x), F.dexp(y)), {==})