def fmod_value

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

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

557def fmod_value(+x: F.F64, +y: F.F64) -> SF.Fmod.value(x, y):
558  +e1 = Equal.cong(Bool, F.F64, t => F.fmod_bad(x, y, t), Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)), SF.rbad(x, y), badv(x, y))
559  Equal.trans(F.F64, F.fmod(x, y), F.fmod_bad(x, y, SF.rbad(x, y)), SF.fmod(x, y), e1, fb_c(x, y, SF.rbad(x, y), {==}))