def ff_c

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

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

529def ff_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +far: Bool, +hfar: {Nat.is_lt(F.dexp(x), F.dexp(y)) == far : Bool}) -> {F.fmod_fin(x, y, far) == FM(x, y) : F.F64}:
530  match far:
531    case True{}:
532      Equal.sym(F.F64, FM(x, y), x, fm_far(x, y, xlt(x, y, True{}, hfar), ok_fin(x, y, h)))
533    case False{}:
534      fm_near(x, y, ok_zy(x, y, h), hfar)