def remainder_value

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

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

781def remainder_value(+x: F.F64, +y: F.F64) -> SF.Remainder.value(x, y):
782  +e1 = Equal.cong(Bool, F.F64, t => F.rm_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))
783  Equal.trans(F.F64, F.remainder(x, y), F.rm_bad(x, y, SF.rbad(x, y)), SF.remainder(x, y), e1, rb_c(x, y, SF.rbad(x, y), {==}))